let z be R_eal; :: thesis: ( z = x / y iff ( ex a, b being Real st
( x = a & y = b & z = a / b ) or ( ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) & z = +infty ) or ( ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) & z = -infty ) or ( ( y = -infty or y = +infty ) & z = 0. ) ) )
thus ( not z = x / y or ex a, b being Real st
( x = a & y = b & z = a / b ) or ( ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) & z = +infty ) or ( ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) & z = -infty ) or ( ( y = -infty or y = +infty ) & z = 0. ) ) :: thesis: ( ( ex a, b being Real st
( x = a & y = b & z = a / b ) or ( ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) & z = +infty ) or ( ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) & z = -infty ) or ( ( y = -infty or y = +infty ) & z = 0. ) ) implies z = x / y )

proof

assume Z: z = x / y ; :: thesis: ( ex a, b being Real st
( x = a & y = b & z = a / b ) or ( ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) & z = +infty ) or ( ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) & z = -infty ) or ( ( y = -infty or y = +infty ) & z = 0. ) )

now

per cases ( ( x in REAL & y in REAL ) or ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) or ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) or y = -infty or y = +infty ) by A1, XXREAL_0:14;

case C: ( x in REAL & y in REAL ) ; :: thesis: ex a, b being Real st
( x = a & y = b & z = a / b )

then consider c being complex number such that
W1: ( y = c & y " = c " ) by XXREAL_3:def 4;
reconsider yy = y, xx = x as Real by C;
reconsider y1 = yy " as Real ;
consider a, b being complex number such that
W2: ( x = a & y " = b & x * (y " ) = a * b ) by C, W1, XXREAL_3:def 2;
z = xx / yy by W2, Z, W1;
hence ex a, b being Real st
( x = a & y = b & z = a / b ) ; :: thesis: verum

end;

case pc: ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) ; :: thesis: verum

per cases ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) by pc;

suppose C: ( x = +infty & 0. < y ) ; :: thesis: z = +infty

then reconsider y = y as Real by A1, XXREAL_0:14;
reconsider yy = y as complex number ;
x / y = +infty by C, XXREAL_3:def 2;
hence z = +infty by Z; :: thesis: verum

end;

suppose C: ( x = -infty & y < 0. ) ; :: thesis: z = +infty

then reconsider y = y as Real by A1, XXREAL_0:14;
reconsider yy = y as complex number ;
x / y = +infty by C, XXREAL_3:def 2;
hence z = +infty by Z; :: thesis: verum

end;

end;

end;

case pc: ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) ; :: thesis: verum

per cases ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) by pc;

suppose C: ( x = -infty & 0. < y ) ; :: thesis: z = -infty

then reconsider y = y as Real by A1, XXREAL_0:14;
reconsider yy = y as complex number ;
x / y = -infty by C, XXREAL_3:def 2;
hence z = -infty by Z; :: thesis: verum

end;

suppose C: ( x = +infty & y < 0. ) ; :: thesis: z = -infty

then reconsider y = y as Real by A1, XXREAL_0:14;
reconsider yy = y as complex number ;
x / y = -infty by C, XXREAL_3:def 2;
hence z = -infty by Z; :: thesis: verum

end;

end;

end;

case ( y = -infty or y = +infty ) ; :: thesis: z = 0.

then y " = 0 by XXREAL_3:def 4;
hence z = 0. by Z, XXREAL_3:1; :: thesis: verum

end;

end;

end;

hence ( ex a, b being Real st
( x = a & y = b & z = a / b ) or ( ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) & z = +infty ) or ( ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) & z = -infty ) or ( ( y = -infty or y = +infty ) & z = 0. ) ) ; :: thesis: verum

end;

assume Z: ( ex a, b being Real st
( x = a & y = b & z = a / b ) or ( ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) & z = +infty ) or ( ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) & z = -infty ) or ( ( y = -infty or y = +infty ) & z = 0. ) ) ; :: thesis: z = x / y

per cases ( ex a, b being Real st
( x = a & y = b & z = a / b ) or ( ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) & z = +infty ) or ( ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) & z = -infty ) or ( ( y = -infty or y = +infty ) & z = 0. ) ) by Z;

suppose ex a, b being Real st
( x = a & y = b & z = a / b ) ; :: thesis: z = x / y

then consider a, b being Real such that
W1: ( x = a & y = b & z = a / b ) ;
reconsider xx = x, yy = y as real number by W1;
Y: yy " = b " by W1;
then ( x is real & y " is real ) by W1;
then reconsider y1 = y " as real number ;
z = xx * y1 by Y, W1;
then z = x * (y " ) ;
hence z = x / y ; :: thesis: verum

end;

suppose S: ( ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) & z = +infty ) ; :: thesis: z = x / y

per cases ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) by S;

suppose S1: ( x = +infty & 0. < y ) ; :: thesis: z = x / y

then reconsider yy = y as positive Real by A1, XXREAL_0:14;
y in REAL by A1, S1, XXREAL_0:14;
then ex a being complex number st
( y = a & y " = a " ) by XXREAL_3:def 4;
then U: yy " = y " ;
y " is positive by U;
hence z = x / y by S1, S, XXREAL_3:def 2; :: thesis: verum

end;

suppose S1: ( x = -infty & y < 0. ) ; :: thesis: z = x / y

then reconsider yy = y as Real by A1, XXREAL_0:14;
y in REAL by A1, S1, XXREAL_0:14;
then ex a being complex number st
( y = a & y " = a " ) by XXREAL_3:def 4;
then U: yy " = y " ;
y is negative by S1;
then y " is negative by U;
hence z = x / y by S1, S, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

suppose S: ( ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) & z = -infty ) ; :: thesis: z = x / y

per cases ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) by S;

suppose S1: ( x = -infty & 0. < y ) ; :: thesis: z = x / y

then reconsider yy = y as positive Real by A1, XXREAL_0:14;
y in REAL by A1, S1, XXREAL_0:14;
then ex a being complex number st
( y = a & y " = a " ) by XXREAL_3:def 4;
then U: yy " = y " ;
y " is positive by U;
hence z = x / y by S1, S, XXREAL_3:def 2; :: thesis: verum

end;

suppose S1: ( x = +infty & y < 0. ) ; :: thesis: z = x / y

then reconsider yy = y as Real by A1, XXREAL_0:14;
y in REAL by A1, S1, XXREAL_0:14;
then ex a being complex number st
( y = a & y " = a " ) by XXREAL_3:def 4;
then U: yy " = y " ;
y is negative by S1;
then y " is negative by U;
hence z = x / y by S1, S, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

suppose S: ( ( y = -infty or y = +infty ) & z = 0. ) ; :: thesis: z = x / y

then y " = 0 by XXREAL_3:def 4;
then x * (y " ) = 0 by XXREAL_3:1;
hence z = x / y by S; :: thesis: verum

end;

end;