:: deftheorem Def12 defines LModlmult LMOD_XX1:def 12 :
for R being Ring
for M being AbGroup
for s being Function of R,(End_Ring M)
for b₄ being Function of [: the carrier of R, the carrier of M:], the carrier of M holds
( b₄ = LModlmult (M,s) iff for x being Element of the carrier of R
for y being Element of the carrier of M ex h being Endomorphism of M st
( h = s . x & b₄ . (x,y) = h . y ) );