let g1, g2 be Element of set_End M; :: thesis: ( ( for x being Element of M holds g1 . x = f . (- x) ) & ( for x being Element of M holds g2 . x = f . (- x) ) implies g1 = g2 )
assume that
A7: for x being Element of M holds g1 . x = f . (- x) and
A8: for x being Element of M holds g2 . x = f . (- x) ; :: thesis: g1 = g2
A9: ( g1 in set_End M & g2 in set_End M ) ;
then consider gg1 being Function of M,M such that
A10: ( gg1 = g1 & gg1 is Endomorphism of M ) ;
consider gg2 being Function of M,M such that
A11: ( gg2 = g2 & gg2 is additive Function of M,M ) by A9;
A12: dom gg2 = the carrier of M by FUNCT_2:def 1;
for x being object st x in dom g1 holds
g1 . x = g2 . x

proof

let x be object ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume x in dom g1 ; :: thesis: g1 . x = g2 . x
then reconsider x0 = x as Element of M by FUNCT_2:def 1, A10;
g1 . x = f . (- x0) by A7
.= g2 . x by A8 ;
hence g1 . x = g2 . x ; :: thesis: verum

end;

hence g1 = g2 by FUNCT_2:def 1, A12, A10, A11; :: thesis: verum