let f be ext-real number ; :: 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 number ;
consider a being complex number such that
A2: f = a and
A3: f " = a " by A1, XXREAL_3:def 4;
A4: (- a) " = - (a " ) by XCMPLX_1:224;
A5: - f = - g ;
ex m being complex number st
( - f = m & - (f " ) = m " )

proof

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

end;

hence (- f) " = - (f " ) by A5, XXREAL_3:def 4; :: thesis: verum

end;

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

hence (- f) " = -infty " by XXREAL_3:def 3
.= - 0
.= - (f " ) by A6 ;
:: thesis: verum

end;

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

hence (- f) " = +infty " by XXREAL_3:def 3
.= - 0
.= - (f " ) by A7 ;
:: thesis: verum

end;

end;