:: deftheorem Def32 defines LCAdd ZMODUL02:def 32 :
for R being Ring
for V being LeftMod of R
for b₃ being BinOp of (LinComb V) holds
( b₃ = LCAdd V iff for e1, e2 being Element of LinComb V holds b₃ . (e1,e2) = (@ e1) + (@ e2) );