theorem Th2: :: LMODFREE:2

for R being Ring
for X being set
for a being Element of the carrier of R
for f, h being Element of Funcs (X, the carrier of R) holds
( h = (LMULT (X,R)) . (a,f) iff for x being object st x in X holds
h . x = the multF of R . (a,(f . x)) )