theorem Th22: :: LMOD_XX1:22

for R being comRing
for M, N being LeftMod of R
for a being Element of the carrier of R
for f being Homomorphism of R,M,N holds
( (lmult_Hom (M,N)) . [a,f] = (LMULT (M,N)) . [a,f] & (LMULT (M,N)) . [a,f] is Homomorphism of R,M,N )