let x be ExtReal; :: thesis: ( x <> -infty & x <> +infty & x <> 0 implies x / x = 1 )
assume ( x <> -infty & x <> +infty ) ; :: thesis: ( not x <> 0 or x / x = 1 )
then x in REAL by XXREAL_0:14;
then reconsider a = x as Real ;
assume x <> 0 ; :: thesis: x / x = 1
then a / a = 1 by XCMPLX_1:60;
hence x / x = 1 ; :: thesis: verum