:: deftheorem Def7 defines LMULT LMODFREE:def 7 :
for R being Ring
for X being set
for b₃ being Function of [: the carrier of R,(Funcs (X, the carrier of R)):],(Funcs (X, the carrier of R)) holds
( b₃ = LMULT (X,R) iff for a being Element of the carrier of R
for f being Element of Funcs (X, the carrier of R)
for x being object st x in X holds
(b₃ . (a,f)) . x = the multF of R . (a,(f . x)) );