theorem Th33: :: SEQFUNC:34

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
for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) by Th30;