:: deftheorem Def32 defines LCAdd ZMODUL02:def 32 :
for V being Z_Module
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) );