theorem :: SEQFUNC:24

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