deffunc H₁( Element of M) -> set = f . (- $1);
consider g being Function such that
A1: ( dom g = the carrier of M & ( for x being Element of M holds g . x = H₁(x) ) ) from FUNCT_1:sch 4();
f in set_End M ;
then consider f1 being Function of M,M such that
A2: ( f1 = f & f1 is Endomorphism of M ) ;
g in set_End M

proof

A3: for o being object st o in the carrier of M holds
g . o in the carrier of M

proof

let o be object ; :: thesis: ( o in the carrier of M implies g . o in the carrier of M )
assume o in the carrier of M ; :: thesis: g . o in the carrier of M
then reconsider o = o as Element of the carrier of M ;
g . o = f1 . (- o) by A1, A2;
hence g . o in the carrier of M ; :: thesis: verum

end;

reconsider g = g as Function of the carrier of M, the carrier of M by A3, A1, FUNCT_2:3;
for x, y being Element of the carrier of M holds g . (x + y) = (g . x) + (g . y)

proof

let x, y be Element of M; :: thesis: g . (x + y) = (g . x) + (g . y)
reconsider z = x + y as Element of M ;
A5: ( f1 . (- x) = g . x & f1 . (- y) = g . y ) by A1, A2;
A6: - z = (- x) - y by VECTSP_1:17
.= (- x) + (- y) ;
g . (x + y) = f1 . ((- x) + (- y)) by A1, A2, A6
.= (g . x) + (g . y) by A5, A2, VECTSP_1:def 20 ;
hence g . (x + y) = (g . x) + (g . y) ; :: thesis: verum

end;

then g is additive ;
hence g in set_End M ; :: thesis: verum

end;

then reconsider g = g as Element of set_End M ;
take g ; :: thesis: for x being Element of M holds g . x = f . (- x)
thus for x being Element of M holds g . x = f . (- x) by A1; :: thesis: verum