for X being set
for H being Functional_Sequence of REAL,REAL st H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is continuous ) holds
(lim (H,X)) | X is continuous