theorem :: SEQFUNC2:34

for X being set
for V, W being RealNormSpace
for H being Functional_Sequence of the carrier of V, the carrier of W st H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is_continuous_on X ) holds
lim (H,X) is_continuous_on X