let r be real number ; :: thesis: for f, g being ext-real number st r + f = r + g holds
f = g
let f, g be ext-real number ; :: thesis: ( r + f = r + g implies f = g )
assume A1: r + f = r + g ; :: thesis: f = g

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

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

then consider a, b being complex number such that
A4: ( r = a & f = b ) and
A5: r + f = a + b by Def3;

now

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

end;

then ex c, d being complex number st
( r = c & g = d & r + g = c + d ) by Def3;
hence f = g by A1, A4, A5; :: thesis: verum

end;

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

then r + f = +infty by Def3;
hence f = g by A1, A6, LTh8; :: thesis: verum

end;

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

then r + f = -infty by Def3;
hence f = g by A1, A7, LTh9; :: thesis: verum

end;

end;