let r be Real; :: thesis: for f, g being ExtReal st r + f = r + g holds
f = g
let f, g be ExtReal; :: 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 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; :: thesis: verum

end;

then A3: ex c, d being Complex st
( r = c & g = d & r + g = c + d ) by Def2;
ex a, b being Complex st
( r = a & f = b & r + f = a + b ) by A2, Def2;
hence f = g by A1, A3; :: thesis: verum

end;

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

then r + f = +infty by Def2;
hence f = g by A1, A4, Lm8; :: thesis: verum

end;

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

then r + f = -infty by Def2;
hence f = g by A1, A5, Lm9; :: thesis: verum

end;

end;