:: deftheorem Def16 defines LMULT LMOD_XX1:def 16 :
for R being Ring
for M, N being LeftMod of R
for b₄ being Function of [: the carrier of R,(Funcs ( the carrier of M, the carrier of N)):],(Funcs ( the carrier of M, the carrier of N)) holds
( b₄ = LMULT (M,N) iff for a being Element of the carrier of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for x being Element of the carrier of M holds (b₄ . [a,f]) . x = a * (f . x) );