(⌊n, \fst (a n)⌋ : sequence O) uniform_converges (\fst x) →
a uniform_converges x.
intros 7; cases H1; cases H2; clear H2 H1;
(⌊n, \fst (a n)⌋ : sequence O) uniform_converges (\fst x) →
a uniform_converges x.
intros 7; cases H1; cases H2; clear H2 H1;