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

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 A2, A3, A4, Def5; :: thesis: verum

end;

then A5: ex c, d being Complex st
( r = c & g = d & r * g = c * d ) by Def5;
ex a, b being Complex st
( r = a & f = b & r * f = a * b ) by A4, Def5;
hence f = g by A1, A2, A5, XCMPLX_1:5; :: thesis: verum

end;

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

assume f <> g ; :: thesis: contradiction
then ( g in REAL or g = -infty ) by A6, XXREAL_0:14;
hence contradiction by A2, A3, A6, Def5; :: 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 A2, A3, A7, Def5; :: thesis: verum

end;

end;