let i1, j1 be Nat; :: thesis: quotient (i1,j1) = i1 / j1

set x = quotient (i1,j1);

set x = quotient (i1,j1);

per cases
( j1 = {} or j1 <> 0 )
;

end;

suppose A2:
j1 <> 0
; :: thesis: quotient (i1,j1) = i1 / j1

+ ((In (0,REAL)),(opp (In (0,REAL)))) = 0
by ARYTM_0:def 3;

then A3: opp (In (0,REAL)) = 0 by ARYTM_0:11;

reconsider y = 1 as Element of REAL by NUMBERS:19;

j1 * (j1 ") = 1 by A2, XCMPLX_0:def 7;

then consider x1, x2, y1, y2 being Element of REAL such that

A4: j1 = [*x1,x2*] and

A5: j1 " = [*y1,y2*] and

A6: y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def 5;

A7: j1 in REAL by XREAL_0:def 1;

+ ((* (x1,y2)),(* (x2,y1))) = 0 by A6, ARYTM_0:24;

then A8: 1 = + ((* (x1,y1)),(opp (* (x2,y2)))) by A6, ARYTM_0:def 5

.= + ((* (x1,y1)),(opp (In (0,REAL)))) by A4, ARYTM_0:12, ARYTM_0:24, A7

.= * (x1,y1) by A3, ARYTM_0:11 ;

j1 in REAL by XREAL_0:def 1;

then x2 = 0 by A4, ARYTM_0:24;

then A9: j1 = x1 by A4, ARYTM_0:def 5;

then x1 in omega by ORDINAL1:def 12;

then reconsider xx = x1 as Element of RAT+ by Lm1;

consider yy being Element of RAT+ such that

A10: xx *' yy = one by A2, A9, ARYTM_3:54;

reconsider xx1 = xx, yy1 = yy as Element of REAL+ by ARYTM_2:1;

A11: ex x9, y9 being Element of RAT+ st

( xx1 = x9 & yy1 = y9 & xx1 *' yy1 = x9 *' y9 ) by ARYTM_2:21;

reconsider xx1 = xx1, yy1 = yy1 as Element of REAL by ARYTM_0:1;

ex x9, y9 being Element of REAL+ st

( xx1 = x9 & yy1 = y9 & * (xx1,yy1) = x9 *' y9 ) by ARYTM_0:def 2;

then A12: yy = y1 by A2, A9, A8, A10, A11, ARYTM_0:18;

then A13: y1 in RAT+ ;

j1 " in REAL by XREAL_0:def 1;

then y2 = 0 by A5, ARYTM_0:24;

then A14: j1 " = y1 by A5, ARYTM_0:def 5;

A15: j1 in omega by ORDINAL1:def 12;

then reconsider a = quotient (i1,j1), b = j1 as Element of RAT+ by Lm1;

consider x91, x92, y91, y92 being Element of REAL such that

A16: i1 = [*x91,x92*] and

A17: j1 " = [*y91,y92*] and

A18: i1 * (j1 ") = [*(+ ((* (x91,y91)),(opp (* (x92,y92))))),(+ ((* (x91,y92)),(* (x92,y91))))*] by XCMPLX_0:def 5;

i1 * (j1 ") in REAL by XREAL_0:def 1;

then A19: + ((* (x91,y92)),(* (x92,y91))) = 0 by A18, ARYTM_0:24;

x1 in omega by A9, ORDINAL1:def 12;

then consider x19, y19 being Element of REAL+ such that

A20: x1 = x19 and

A21: y1 = y19 and

A22: * (x1,y1) = x19 *' y19 by A13, ARYTM_0:def 2, ARYTM_2:1, ARYTM_2:2;

A23: ex x199, y199 being Element of RAT+ st

( x19 = x199 & y19 = y199 & x19 *' y19 = x199 *' y199 ) by A9, A12, A15, A20, A21, Lm1, ARYTM_2:21;

j1 " in REAL by XREAL_0:def 1;

then A24: y92 = 0 by A17, ARYTM_0:24;

then j1 " = y91 by A17, ARYTM_0:def 5;

then A25: i1 * (j1 ") = + ((* (x91,y1)),(opp (* (x92,(In (0,REAL)))))) by A14, A18, A24, A19, ARYTM_0:def 5

.= + ((* (x91,y1)),(In (0,REAL))) by A3, ARYTM_0:12

.= * (x91,y1) by ARYTM_0:11 ;

i1 in REAL by XREAL_0:def 1;

then x92 = 0 by A16, ARYTM_0:24;

then A26: i1 = x91 by A16, ARYTM_0:def 5;

then A27: x91 in omega by ORDINAL1:def 12;

then x91 in RAT+ by Lm1;

then consider x9, y9 being Element of REAL+ such that

A28: x91 = x9 and

A29: y1 = y9 and

A30: i1 * (j1 ") = x9 *' y9 by A25, A13, ARYTM_0:def 2, ARYTM_2:1;

consider x99, y99 being Element of RAT+ such that

A31: x9 = x99 and

A32: y9 = y99 and

A33: i1 * (j1 ") = x99 *' y99 by A27, A12, A28, A29, A30, Lm1, ARYTM_2:21;

a *' b = (quotient (i1,j1)) *' (quotient (j1,one)) by ARYTM_3:40

.= quotient ((i1 *^ j1),(j1 *^ one)) by ARYTM_3:49

.= (quotient (i1,one)) *' (quotient (j1,j1)) by ARYTM_3:49

.= (quotient (i1,one)) *' one by A2, ARYTM_3:41

.= quotient (i1,one) by ARYTM_3:53

.= i1 by ARYTM_3:40

.= x99 *' one by A26, A28, A31, ARYTM_3:53

.= (x99 *' y99) *' b by A9, A8, A29, A32, A20, A21, A22, A23, ARYTM_3:52 ;

hence quotient (i1,j1) = i1 / j1 by A2, A33, ARYTM_3:56; :: thesis: verum

end;then A3: opp (In (0,REAL)) = 0 by ARYTM_0:11;

reconsider y = 1 as Element of REAL by NUMBERS:19;

j1 * (j1 ") = 1 by A2, XCMPLX_0:def 7;

then consider x1, x2, y1, y2 being Element of REAL such that

A4: j1 = [*x1,x2*] and

A5: j1 " = [*y1,y2*] and

A6: y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def 5;

A7: j1 in REAL by XREAL_0:def 1;

+ ((* (x1,y2)),(* (x2,y1))) = 0 by A6, ARYTM_0:24;

then A8: 1 = + ((* (x1,y1)),(opp (* (x2,y2)))) by A6, ARYTM_0:def 5

.= + ((* (x1,y1)),(opp (In (0,REAL)))) by A4, ARYTM_0:12, ARYTM_0:24, A7

.= * (x1,y1) by A3, ARYTM_0:11 ;

j1 in REAL by XREAL_0:def 1;

then x2 = 0 by A4, ARYTM_0:24;

then A9: j1 = x1 by A4, ARYTM_0:def 5;

then x1 in omega by ORDINAL1:def 12;

then reconsider xx = x1 as Element of RAT+ by Lm1;

consider yy being Element of RAT+ such that

A10: xx *' yy = one by A2, A9, ARYTM_3:54;

reconsider xx1 = xx, yy1 = yy as Element of REAL+ by ARYTM_2:1;

A11: ex x9, y9 being Element of RAT+ st

( xx1 = x9 & yy1 = y9 & xx1 *' yy1 = x9 *' y9 ) by ARYTM_2:21;

reconsider xx1 = xx1, yy1 = yy1 as Element of REAL by ARYTM_0:1;

ex x9, y9 being Element of REAL+ st

( xx1 = x9 & yy1 = y9 & * (xx1,yy1) = x9 *' y9 ) by ARYTM_0:def 2;

then A12: yy = y1 by A2, A9, A8, A10, A11, ARYTM_0:18;

then A13: y1 in RAT+ ;

j1 " in REAL by XREAL_0:def 1;

then y2 = 0 by A5, ARYTM_0:24;

then A14: j1 " = y1 by A5, ARYTM_0:def 5;

A15: j1 in omega by ORDINAL1:def 12;

then reconsider a = quotient (i1,j1), b = j1 as Element of RAT+ by Lm1;

consider x91, x92, y91, y92 being Element of REAL such that

A16: i1 = [*x91,x92*] and

A17: j1 " = [*y91,y92*] and

A18: i1 * (j1 ") = [*(+ ((* (x91,y91)),(opp (* (x92,y92))))),(+ ((* (x91,y92)),(* (x92,y91))))*] by XCMPLX_0:def 5;

i1 * (j1 ") in REAL by XREAL_0:def 1;

then A19: + ((* (x91,y92)),(* (x92,y91))) = 0 by A18, ARYTM_0:24;

x1 in omega by A9, ORDINAL1:def 12;

then consider x19, y19 being Element of REAL+ such that

A20: x1 = x19 and

A21: y1 = y19 and

A22: * (x1,y1) = x19 *' y19 by A13, ARYTM_0:def 2, ARYTM_2:1, ARYTM_2:2;

A23: ex x199, y199 being Element of RAT+ st

( x19 = x199 & y19 = y199 & x19 *' y19 = x199 *' y199 ) by A9, A12, A15, A20, A21, Lm1, ARYTM_2:21;

j1 " in REAL by XREAL_0:def 1;

then A24: y92 = 0 by A17, ARYTM_0:24;

then j1 " = y91 by A17, ARYTM_0:def 5;

then A25: i1 * (j1 ") = + ((* (x91,y1)),(opp (* (x92,(In (0,REAL)))))) by A14, A18, A24, A19, ARYTM_0:def 5

.= + ((* (x91,y1)),(In (0,REAL))) by A3, ARYTM_0:12

.= * (x91,y1) by ARYTM_0:11 ;

i1 in REAL by XREAL_0:def 1;

then x92 = 0 by A16, ARYTM_0:24;

then A26: i1 = x91 by A16, ARYTM_0:def 5;

then A27: x91 in omega by ORDINAL1:def 12;

then x91 in RAT+ by Lm1;

then consider x9, y9 being Element of REAL+ such that

A28: x91 = x9 and

A29: y1 = y9 and

A30: i1 * (j1 ") = x9 *' y9 by A25, A13, ARYTM_0:def 2, ARYTM_2:1;

consider x99, y99 being Element of RAT+ such that

A31: x9 = x99 and

A32: y9 = y99 and

A33: i1 * (j1 ") = x99 *' y99 by A27, A12, A28, A29, A30, Lm1, ARYTM_2:21;

a *' b = (quotient (i1,j1)) *' (quotient (j1,one)) by ARYTM_3:40

.= quotient ((i1 *^ j1),(j1 *^ one)) by ARYTM_3:49

.= (quotient (i1,one)) *' (quotient (j1,j1)) by ARYTM_3:49

.= (quotient (i1,one)) *' one by A2, ARYTM_3:41

.= quotient (i1,one) by ARYTM_3:53

.= i1 by ARYTM_3:40

.= x99 *' one by A26, A28, A31, ARYTM_3:53

.= (x99 *' y99) *' b by A9, A8, A29, A32, A20, A21, A22, A23, ARYTM_3:52 ;

hence quotient (i1,j1) = i1 / j1 by A2, A33, ARYTM_3:56; :: thesis: verum