let r be real number ; :: thesis: for f, g being ext-real number st r <> 0 & r * f = r * g holds
f = g
let f, g be ext-real number ; :: thesis: ( r <> 0 & r * f = r * g implies f = g )
assume that
A1: r <> 0 and
A2: r * f = r * g ; :: thesis: f = g
A3: ( r is positive or r is negative ) by A1;

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

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

then consider a, b being complex number such that
A5: ( r = a & f = b ) and
A6: r * f = a * b by Def4;

now

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

end;

then ex c, d being complex number st
( r = c & g = d & r * g = c * d ) by Def4;
hence f = g by A1, A2, A5, A6, XCMPLX_1:5; :: thesis: verum

end;

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

assume f <> g ; :: thesis: contradiction
then ( g in REAL or g = -infty ) by A7, XXREAL_0:14;
hence contradiction by A3, A2, A7, Def4; :: thesis: verum

end;

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

assume f <> g ; :: thesis: contradiction
then ( g in REAL or g = +infty ) by A9, XXREAL_0:14;
hence contradiction by A3, A2, A9, Def4; :: thesis: verum

end;

end;