theorem :: SEQFUNC:40

for D being non empty set
for H1, H2 being Functional_Sequence of D,REAL
for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds
( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) & H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) )