let x, y be ExtReal; :: thesis: ( -infty <> y & y <> +infty & y <> 0 implies ( (x * y) / y = x & x * (y / y) = x ) )
assume that
A1: -infty <> y and
A2: y <> +infty and
A3: y <> 0 ; :: thesis: ( (x * y) / y = x & x * (y / y) = x )
reconsider b = y as Element of REAL by A1, A2, XXREAL_0:14;
A4: (x * y) / y = x

proof

per cases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;

suppose A5: x = +infty ; :: thesis: (x * y) / y = x

per cases ( 0 < y or y < 0 ) by A3;

suppose A6: 0 < y ; :: thesis: (x * y) / y = x

then x * y = +infty by A5, Def5;
hence (x * y) / y = x by A2, A5, A6, Th83; :: thesis: verum

end;

suppose A7: y < 0 ; :: thesis: (x * y) / y = x

then x * y = -infty by A5, Def5;
hence (x * y) / y = x by A1, A5, A7, Th84; :: thesis: verum

end;

end;

end;

suppose A8: x = -infty ; :: thesis: (x * y) / y = x

per cases ( 0 < y or y < 0 ) by A3;

suppose A9: 0 < y ; :: thesis: (x * y) / y = x

then x * y = -infty by A8, Def5;
hence (x * y) / y = x by A2, A8, A9, Th86; :: thesis: verum

end;

suppose A10: y < 0 ; :: thesis: (x * y) / y = x

then x * y = +infty by A8, Def5;
hence (x * y) / y = x by A1, A8, A10, Th85; :: thesis: verum

end;

end;

end;

suppose ( x <> +infty & x <> -infty ) ; :: thesis: (x * y) / y = x

then x in REAL by XXREAL_0:14;
then reconsider a = x as Real ;
(x * y) / y = (a * b) / b
.= a by A3, XCMPLX_1:89 ;
hence (x * y) / y = x ; :: thesis: verum

end;

end;

end;

y / y = 1 by A1, A2, A3, Th78;
hence ( (x * y) / y = x & x * (y / y) = x ) by A4, Th81; :: thesis: verum