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) & (add_End M) . [f,g] = (ADD (M,M)) . (f,g) & (ADD (M,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) & (add_End M) . [f,g] = (ADD (M,M)) . (f,g) & (ADD (M,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) & (add_End M) . [f,g] = (ADD (M,M)) . (f,g) & (ADD (M,M)) . (f,g) is Endomorphism of M ) by Th2, ZFMISC_1:87, FUNCT_1:49; :: thesis: verum