theorem :: SEQFUNC:6

for D being non empty set
for G, H, J being Functional_Sequence of D,REAL holds
( (G + H) (#) J = (G (#) J) + (H (#) J) & J (#) (G + H) = (J (#) G) + (J (#) H) )