theorem :: SEQFUNC2:3

for D being non empty set
for Y being RealNormSpace
for G, H, J being Functional_Sequence of D, the carrier of Y holds
( G + H = H + G & (G + H) + J = G + (H + J) )