:: deftheorem Def5 defines + SEQFUNC:def 5 :
for D being non empty set
for G, H, b₄ being Functional_Sequence of D,REAL holds
( b₄ = G + H iff for n being Nat holds b₄ . n = (G . n) + (H . n) );