:: deftheorem defines + LMOD_7:def 10 :
for K being Ring
for V being LeftMod of K
for A1, A2, b₅ being Subset of V holds
( b₅ = A1 + A2 iff for x being set holds
( x in b₅ iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) );