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;