:: deftheorem defines LMULT LMODFREE:def 3 :
for R being Ring
for X being set
for N being LeftMod of R
for b₄ being Function of [: the carrier of R,(Funcs (X, the carrier of N)):],(Funcs (X, the carrier of N)) holds
( b₄ = LMULT (X,N) iff for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of N)
for x being object st x in X holds
(b₄ . (a,f)) . x = the lmult of N . (a,(f . x)) );