:: deftheorem Def15 defines + LMOD_7:def 15 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for S1, S2, b₆ being Element of V .. W holds
( b₆ = S1 + S2 iff for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
b₆ = (a1 + a2) .. W );