let f be ExtReal; :: thesis: (- f) " = - (f ")

per cases ( f in REAL or f = +infty or f = -infty ) by XXREAL_0:14;

suppose A1: f in REAL ; :: thesis: (- f) " = - (f ")

then reconsider g = f as Real ;
A2: - f = - g ;
consider a being Complex such that
A3: f = a and
A4: f " = a " by A1, Def6;
A5: (- a) " = - (a ") by XCMPLX_1:222;
ex m being Complex st
( - f = m & - (f ") = m " )

proof

take - a ; :: thesis: ( - f = - a & - (f ") = (- a) " )
thus - f = - a by A3, A2; :: thesis: - (f ") = (- a) "
thus - (f ") = (- a) " by A4, A5, A2, Def3; :: thesis: verum

end;

hence (- f) " = - (f ") by A2, Def6; :: thesis: verum

end;

suppose A6: f = +infty ; :: thesis: (- f) " = - (f ")

hence (- f) " = -infty " by Def3
.= - (f ") by A6 ;
:: thesis: verum

end;

suppose A7: f = -infty ; :: thesis: (- f) " = - (f ")

hence (- f) " = +infty " by Def3
.= - (f ") by A7 ;
:: thesis: verum

end;

end;