let M be AbGroup; :: thesis: for f being Element of set_End M holds (ADD (M,M)) . (f,(Inv f)) = ZeroMap (M,M)
let f be Element of set_End M; :: thesis: (ADD (M,M)) . (f,(Inv f)) = ZeroMap (M,M)
f in set_End M ;
then consider f1 being Function of the carrier of M, the carrier of M such that
A1: ( f1 = f & f1 is Endomorphism of M ) ;
Inv f in set_End M ;
then consider g1 being Function of the carrier of M, the carrier of M such that
A2: ( g1 = Inv f & g1 is Endomorphism of M ) ;
reconsider f1 = f1, g1 = g1 as Element of Funcs ( the carrier of M, the carrier of M) by FUNCT_2:8;
for x being Element of the carrier of M holds ((ADD (M,M)) . (f1,g1)) . x = (ZeroMap (M,M)) . x

proof

let x be Element of the carrier of M; :: thesis: ((ADD (M,M)) . (f1,g1)) . x = (ZeroMap (M,M)) . x
A3: g1 . x = f1 . (- x) by A1, A2, Def8;
A4: (f1 . (0. M)) + (f1 . (0. M)) = f1 . ((0. M) + (0. M)) by A1, VECTSP_1:def 20
.= f1 . (0. M) by ALGSTR_1:7
.= (f1 . (0. M)) + (0. M) by ALGSTR_1:7 ;
((ADD (M,M)) . (f1,g1)) . x = (f1 . x) + (f1 . (- x)) by Th1, A3
.= f1 . (x + (- x)) by A1, VECTSP_1:def 20
.= f1 . (0. M) by VECTSP_1:19
.= ( the carrier of M --> (0. M)) . x by A4, RLVECT_1:8
.= (ZeroMap (M,M)) . x by GRCAT_1:def 7 ;
hence ((ADD (M,M)) . (f1,g1)) . x = (ZeroMap (M,M)) . x ; :: thesis: verum

end;

hence (ADD (M,M)) . (f,(Inv f)) = ZeroMap (M,M) by A1, A2; :: thesis: verum