let R be comRing; :: thesis: for M, N being LeftMod of R
for a being Element of the carrier of R
for g being Homomorphism of R,M,N holds (LMULT (M,N)) . [a,g] is Homomorphism of R,M,N
let M, N be LeftMod of R; :: thesis: for a being Element of the carrier of R
for g being Homomorphism of R,M,N holds (LMULT (M,N)) . [a,g] is Homomorphism of R,M,N
let a be Element of the carrier of R; :: thesis: for g being Homomorphism of R,M,N holds (LMULT (M,N)) . [a,g] is Homomorphism of R,M,N
let g be Homomorphism of R,M,N; :: thesis: (LMULT (M,N)) . [a,g] is Homomorphism of R,M,N
reconsider g = g as Element of Funcs ( the carrier of M, the carrier of N) by FUNCT_2:8;
reconsider F = (LMULT (M,N)) . [a,g] as Element of Funcs ( the carrier of M, the carrier of N) ;
A1: for x, y being Element of the carrier of M holds F . (x + y) = (F . x) + (F . y)

proof

let x, y be Element of the carrier of M; :: thesis: F . (x + y) = (F . x) + (F . y)
reconsider z = x + y as Element of the carrier of M ;
F . z = a * (g . (x + y)) by Def16
.= a * ((g . x) + (g . y)) by Def10, VECTSP_1:def 20
.= (a * (g . x)) + (a * (g . y)) by VECTSP_1:def 14
.= (F . x) + (a * (g . y)) by Def16
.= (F . x) + (F . y) by Def16 ;
hence F . (x + y) = (F . x) + (F . y) ; :: thesis: verum

end;

for b being Element of R
for x being Element of the carrier of M holds F . (b * x) = b * (F . x)

proof

let b be Element of R; :: thesis: for x being Element of the carrier of M holds F . (b * x) = b * (F . x)
let x be Element of the carrier of M; :: thesis: F . (b * x) = b * (F . x)
reconsider z = b * x as Element of the carrier of M ;
F . z = a * (g . (b * x)) by Def16
.= a * (b * (g . x)) by Def10, MOD_2:def 2
.= (a * b) * (g . x) by VECTSP_1:def 16
.= b * (a * (g . x)) by VECTSP_1:def 16
.= b * (F . x) by Def16 ;
hence F . (b * x) = b * (F . x) ; :: thesis: verum

end;

then F is homogeneous ;
hence (LMULT (M,N)) . [a,g] is Homomorphism of R,M,N by A1, Def10, VECTSP_1:def 20; :: thesis: verum