theorem Th42: :: SEQFUNC2:33

for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set holds
( H is_unif_conv_on X iff ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - ((lim (H,X)) /. x)).|| < r ) ) )