let y, x be R_eal; :: 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 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

now

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

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

then x * y = +infty by A5, EXTREAL1:def 1;
hence (x * y) / y = x by A2, A5, A6, Th17; :: thesis: verum

end;

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

then x * y = -infty by A5, EXTREAL1:def 1;
hence (x * y) / y = x by A1, A5, A7, Th17; :: thesis: verum

end;

end;

end;

hence (x * y) / y = x ; :: thesis: verum

end;

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

now

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

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

then x * y = -infty by A8, EXTREAL1:def 1;
hence (x * y) / y = x by A2, A8, A9, Th18; :: thesis: verum

end;

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

then x * y = +infty by A8, EXTREAL1:def 1;
hence (x * y) / y = x by A1, A8, A10, Th18; :: thesis: verum

end;

end;

end;

hence (x * y) / y = x ; :: thesis: verum

end;

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

then reconsider a = x as Real by XXREAL_0:14;
x * y = a * b by EXTREAL1:13;
then (x * y) / y = (a * b) / b by A3, EXTREAL1:32
.= a by A3, XCMPLX_1:90 ;
hence (x * y) / y = x ; :: thesis: verum

end;

end;

end;

y / y = 1. by A1, A2, A3, EXTREAL1:34, MESFUNC1:def 8;
hence ( (x * y) / y = x & x * (y / y) = x ) by A4, Th4; :: thesis: verum