:: deftheorem Def15 defines ADD LMOD_XX1:def 15 :
for R being Ring
for M, N being LeftMod of R
for b₄ being BinOp of (Funcs ( the carrier of M, the carrier of N)) holds
( b₄ = ADD (M,N) iff for f, g being Element of Funcs ( the carrier of M, the carrier of N) holds b₄ . (f,g) = the addF of N .: (f,g) );