theorem :: SEQFUNC2:14

for D being non empty set
for Z being set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_point_conv_on X holds
( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )