theorem :: SEQFUNC:4

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) )