:: deftheorem Def2 defines + NORMSP_1:def 2 :
for RNS being non empty addLoopStr
for S1, S2, b₄ being sequence of RNS holds
( b₄ = S1 + S2 iff for n being Nat holds b₄ . n = (S1 . n) + (S2 . n) );