let M, N be AbGroup; :: thesis: for f, g being Homomorphism of M,N holds (ADD (M,N)) . (f,g) is Homomorphism of M,N
let f, g be Homomorphism of M,N; :: thesis: (ADD (M,N)) . (f,g) is Homomorphism of 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) ;
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 Th1
.= ((f . x) + (f . y)) + (g . (x + y)) by VECTSP_1:def 20
.= ((f . x) + (f . y)) + ((g . x) + (g . y)) by 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 Th1
.= (F . x) + ((f . y) + (g . y)) by RLVECT_1:def 3
.= (F . x) + (F . y) by Th1 ;
hence F . (x + y) = (F . x) + (F . y) ; :: thesis: verum

end;

then F is additive ;
hence (ADD (M,N)) . (f,g) is Homomorphism of M,N ; :: thesis: verum