let f, g be ext-real number ; :: thesis: for r being real number st r + f = r + g holds
f = g
let r be real number ; :: thesis: ( r + f = r + g implies f = g )
assume A1: r + f = r + g ; :: thesis: f = g
A2: ( f in ExtREAL & g in ExtREAL & r in ExtREAL ) by XXREAL_0:def 1;

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 XXREAL_3:def 1;

now

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

end;

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

end;

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

then r + f = +infty by XXREAL_3:def 1;
hence f = g by A1, A6, A2, SUPINF_2:8; :: thesis: verum

end;

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

then r + f = -infty by XXREAL_3:def 1;
hence f = g by A1, A7, A2, SUPINF_2:9; :: thesis: verum

end;

end;