:: deftheorem defines - LMOD_7:def 14 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for S1, b₅ being Element of V .. W holds
( b₅ = - S1 iff for a being Vector of V st S1 = a .. W holds
b₅ = (- a) .. W );