theorem :: SEQFUNC:8

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) - (J (#) H) = J (#) (G - H) )