let M be AbGroup; :: thesis: for f, g being Endomorphism of M holds (FuncComp M) . (f,g) is Endomorphism of M
let f, g be Endomorphism of M; :: thesis: (FuncComp M) . (f,g) is Endomorphism of M
reconsider f = f, g = g as Element of Funcs ( the carrier of M, the carrier of M) by FUNCT_2:8;
reconsider F = (FuncComp M) . (f,g) as Element of Funcs ( the carrier of M, the carrier of M) ;
F is additive

proof

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 ;
A1: F . y = (f * g) . y by Def4;
F . (x + y) = (f * g) . z by Def4
.= f . (g . (x + y)) by FUNCT_2:15
.= f . ((g . x) + (g . y)) by VECTSP_1:def 20
.= (f . (g . x)) + (f . (g . y)) by VECTSP_1:def 20
.= ((f * g) . x) + (f . (g . y)) by FUNCT_2:15
.= ((f * g) . x) + ((f * g) . y) by FUNCT_2:15
.= (F . x) + (F . y) by Def4, A1 ;
hence F . (x + y) = (F . x) + (F . y) ; :: thesis: verum

end;

hence F is additive ; :: thesis: verum

end;

hence (FuncComp M) . (f,g) is Endomorphism of M ; :: thesis: verum