let R be comRing; :: thesis: for M, N being LeftMod of R
for f, g being Homomorphism of R,M,N holds (ADD (M,N)) . (f,g) is Homomorphism of R,M,N
let M, N be LeftMod of R; :: thesis: for f, g being Homomorphism of R,M,N holds (ADD (M,N)) . (f,g) is Homomorphism of R,M,N
let f, g be Homomorphism of R,M,N; :: thesis: (ADD (M,N)) . (f,g) is Homomorphism of R,M,N
reconsider f = f, g = g as Element of Funcs ( the carrier of M, the carrier of N) by FUNCT_2:8;
reconsider F = (ADD (M,N)) . (f,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 . (x + y) = (f . (x + y)) + (g . (x + y)) by Th15
.= ((f . x) + (f . y)) + (g . (x + y)) by Def10, VECTSP_1:def 20
.= ((f . x) + (f . y)) + ((g . x) + (g . y)) by Def10, VECTSP_1:def 20
.= (f . x) + ((f . y) + ((g . x) + (g . y))) by RLVECT_1:def 3
.= (f . x) + (((f . y) + (g . x)) + (g . y)) by RLVECT_1:def 3
.= ((f . x) + ((g . x) + (f . y))) + (g . y) by RLVECT_1:def 3
.= (((f . x) + (g . x)) + (f . y)) + (g . y) by RLVECT_1:def 3
.= ((F . x) + (f . y)) + (g . y) by Th15
.= (F . x) + ((f . y) + (g . y)) by RLVECT_1:def 3
.= (F . x) + (F . y) by Th15 ;
hence F . (x + y) = (F . x) + (F . y) ; :: thesis: verum

end;

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

proof

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

end;

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