let R be comRing; :: thesis: for M, N, M1 being LeftMod of R
for f being Homomorphism of R,M,N
for u being Homomorphism of R,M1,M holds f * u is Homomorphism of R,M1,N
let M, N, M1 be LeftMod of R; :: thesis: for f being Homomorphism of R,M,N
for u being Homomorphism of R,M1,M holds f * u is Homomorphism of R,M1,N
let f be Homomorphism of R,M,N; :: thesis: for u being Homomorphism of R,M1,M holds f * u is Homomorphism of R,M1,N
let u be Homomorphism of R,M1,M; :: thesis: f * u is Homomorphism of R,M1,N
A1: for x1, y1 being Element of the carrier of M1
for a being Element of R holds
( (f * u) . (x1 + y1) = ((f * u) . x1) + ((f * u) . y1) & a * ((f * u) . x1) = a * ((f * u) . x1) )

proof

let x1, y1 be Element of the carrier of M1; :: thesis: for a being Element of R holds
( (f * u) . (x1 + y1) = ((f * u) . x1) + ((f * u) . y1) & a * ((f * u) . x1) = a * ((f * u) . x1) )
let a be Element of R; :: thesis: ( (f * u) . (x1 + y1) = ((f * u) . x1) + ((f * u) . y1) & a * ((f * u) . x1) = a * ((f * u) . x1) )
reconsider ux1 = u . x1, uy1 = u . y1 as Element of the carrier of M ;
(f * u) . (x1 + y1) = f . (u . (x1 + y1)) by FUNCT_2:15
.= f . (ux1 + uy1) by Def10, VECTSP_1:def 20
.= (f . ux1) + (f . uy1) by Def10, VECTSP_1:def 20
.= ((f * u) . x1) + (f . (u . y1)) by FUNCT_2:15
.= ((f * u) . x1) + ((f * u) . y1) by FUNCT_2:15 ;
hence ( (f * u) . (x1 + y1) = ((f * u) . x1) + ((f * u) . y1) & a * ((f * u) . x1) = a * ((f * u) . x1) ) ; :: thesis: verum

end;

for x1 being Element of the carrier of M1
for a being Element of R holds (f * u) . (a * x1) = a * ((f * u) . x1)

proof

let x1 be Element of the carrier of M1; :: thesis: for a being Element of R holds (f * u) . (a * x1) = a * ((f * u) . x1)
let a be Element of R; :: thesis: (f * u) . (a * x1) = a * ((f * u) . x1)
reconsider ux1 = u . x1 as Element of the carrier of M ;
(f * u) . (a * x1) = f . (u . (a * x1)) by FUNCT_2:15
.= f . (a * ux1) by Def10, MOD_2:def 2
.= a * (f . ux1) by Def10, MOD_2:def 2
.= a * ((f * u) . x1) by FUNCT_2:15 ;
hence (f * u) . (a * x1) = a * ((f * u) . x1) ; :: thesis: verum

end;

then f * u is homogeneous ;
hence f * u is Homomorphism of R,M1,N by A1, Def10, VECTSP_1:def 20; :: thesis: verum