let M be AbGroup; :: thesis: for f, g being Endomorphism of M holds
( f in Funcs ( the carrier of M, the carrier of M) & g in Funcs ( the carrier of M, the carrier of M) & (mult_End M) . [f,g] = (FuncComp M) . (f,g) & (FuncComp M) . (f,g) is Endomorphism of M )
let f, g be Endomorphism of M; :: thesis: ( f in Funcs ( the carrier of M, the carrier of M) & g in Funcs ( the carrier of M, the carrier of M) & (mult_End M) . [f,g] = (FuncComp M) . (f,g) & (FuncComp M) . (f,g) is Endomorphism of M )
( f in set_End M & g in set_End M ) ;
hence ( f in Funcs ( the carrier of M, the carrier of M) & g in Funcs ( the carrier of M, the carrier of M) & (mult_End M) . [f,g] = (FuncComp M) . (f,g) & (FuncComp M) . (f,g) is Endomorphism of M ) by Th5, ZFMISC_1:87, FUNCT_1:49; :: thesis: verum