let R be comRing; :: thesis: 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 )
let M, N be LeftMod of R; :: thesis: 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 )
let a be Element of the carrier of R; :: thesis: 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 )
let f be Homomorphism of R,M,N; :: thesis: ( (lmult_Hom (M,N)) . [a,f] = (LMULT (M,N)) . [a,f] & (LMULT (M,N)) . [a,f] is Homomorphism of R,M,N )
( a in the carrier of R & f in set_Hom (M,N) ) ;
hence ( (lmult_Hom (M,N)) . [a,f] = (LMULT (M,N)) . [a,f] & (LMULT (M,N)) . [a,f] is Homomorphism of R,M,N ) by ZFMISC_1:87, FUNCT_1:49, Th20; :: thesis: verum