theorem Th16: :: LMOD_XX1:16

for R being Ring
for M, N being LeftMod of R
for a being Element of the carrier of R
for f, h being Element of Funcs ( the carrier of M, the carrier of N) holds
( h = (LMULT (M,N)) . [a,f] iff for x being Element of M holds h . x = a * (f . x) )