theorem Th5: :: SEQFUNC:5

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