:: deftheorem Def17 defines ADD LMOD_7:def 17 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b₄ being BinOp of (V .. W) holds
( b₄ = ADD W iff for S1, S2 being Element of V .. W holds b₄ . (S1,S2) = S1 + S2 );