let r be Real; :: thesis:
let f, g be ExtReal; :: thesis:
assume that
A1: r <> 0 and
A2: r * f = r * g ; :: thesis:
A3: ( r is positive or r is negative ) by A1;

per cases by XXREAL_0:14;

suppose A4: f in REAL ; :: thesis:

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

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:

end;

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

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

end;

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

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

end;

end;