assume A8:
x " = 0
; :: according to ORDINAL1:def 14 :: thesis: contradiction

then A9: x " = In (0,REAL) by Lm1;

x * (x ") = 1 by Def6;

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

x = [*x1,x2*] and

A10: x " = [*y1,y2*] and

A11: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by Def4;

y2 = In (0,REAL) by A8, A10, ARYTM_0:24, Lm1;

then A12: y1 = 0 by A8, A10, ARYTM_0:def 5, Lm1;

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

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

.= + ((* (x1,y1)),(* ((opp x2),y2))) by ARYTM_0:15

.= * ((opp x2),y2) by A12, ARYTM_0:11, ARYTM_0:12 ;

hence contradiction by A10, ARYTM_0:12, ARYTM_0:24, A9; :: thesis: verum

then A9: x " = In (0,REAL) by Lm1;

x * (x ") = 1 by Def6;

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

x = [*x1,x2*] and

A10: x " = [*y1,y2*] and

A11: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by Def4;

y2 = In (0,REAL) by A8, A10, ARYTM_0:24, Lm1;

then A12: y1 = 0 by A8, A10, ARYTM_0:def 5, Lm1;

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

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

.= + ((* (x1,y1)),(* ((opp x2),y2))) by ARYTM_0:15

.= * ((opp x2),y2) by A12, ARYTM_0:11, ARYTM_0:12 ;

hence contradiction by A10, ARYTM_0:12, ARYTM_0:24, A9; :: thesis: verum