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, Def6;
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, Def5; :: thesis: verum

end;

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

end;

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

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

end;

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

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

end;

end;