theorem Th78: :: XXREAL_3:78

for x being ExtReal st x <> -infty & x <> +infty & x <> 0 holds
x / x = 1