:: deftheorem Def6 defines SubJoin RMOD_3:def 6 :
for R being Ring
for V being RightMod of R
for b₃ being BinOp of (Submodules V) holds
( b₃ = SubJoin V iff for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b₃ . (A1,A2) = W1 + W2 );