theorem Th83: :: XXREAL_3:83

for y being ExtReal st 0 < y & y <> +infty holds
+infty / y = +infty