let f, g be ExtReal; :: thesis: ( - f = - g implies f = g )
assume A1: - f = - g ; :: thesis: f = g

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

suppose A2: f in REAL ; :: thesis: f = g

now :: thesis: g in REAL

assume not g in REAL ; :: thesis: contradiction
then ( g = +infty or g = -infty ) by XXREAL_0:14;
hence contradiction by A1, A2, Def3; :: thesis: verum

end;

then A3: ex a being Complex st
( g = a & - g = - a ) by Def3;
ex a being Complex st
( f = a & - f = - a ) by A2, Def3;
hence f = g by A1, A3; :: thesis: verum

end;

suppose f = +infty ; :: thesis: f = g

hence f = g by A1, Th5; :: thesis: verum

end;

suppose f = -infty ; :: thesis: f = g

then - (- g) = -infty by A1;
hence f = g by A1; :: thesis: verum

end;

end;