let x, y be ExtReal; :: thesis: ( y <> +infty & y <> -infty & y <> 0 implies (x / y) * y = x )
assume that
A1: ( y <> +infty & y <> -infty ) and
A2: y <> 0 ; :: thesis: (x / y) * y = x
thus (x / y) * y = (x * (1 / y)) * y by XXREAL_3:81
.= x * ((1 / y) * y) by XXREAL_3:66
.= x * 1 by A1, A2, XXREAL_3:87
.= x by XXREAL_3:81 ; :: thesis: verum