let x be R_eal; :: thesis: ( x <> -infty & x <> +infty & x <> 0. implies x / x = 1 )
assume A1: ( x <> -infty & x <> +infty & x <> 0. ) ; :: thesis: x / x = 1
then consider a, b being Real such that
A2: ( x = a & x = b & x / x = a / b ) by Def2;
thus x / x = 1 by A1, A2, XCMPLX_1:60; :: thesis: verum