let y, x be ext-real number ; :: 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, Def4;
hence (x * y) / y = x by A2, A5, A6, Th81; :: thesis: verum

end;

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

then x * y = -infty by A5, Def4;
hence (x * y) / y = x by A1, A5, A7, Th82; :: 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, Def4;
hence (x * y) / y = x by A2, A8, A9, Th84; :: thesis: verum

end;

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

then x * y = +infty by A8, Def4;
hence (x * y) / y = x by A1, A8, A10, Th83; :: 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 number ;
(x * y) / y = (a * b) / b
.= a by A3, XCMPLX_1:90 ;
hence (x * y) / y = x ; :: thesis: verum

end;

end;

end;

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