:: deftheorem Def3 defines - NORMSP_1:def 3 :
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) );