theorem Th21: :: SEQFUNC:22
for D being non empty set
for H being Functional_Sequence of D,REAL
for X being set st H is_unif_conv_on X holds
H is_point_conv_on X