theorem Th8: :: FVALUAT1:8

for x, y being ExtReal st y <> +infty & y <> -infty & y <> 0 holds
(x / y) * y = x