set j = 1;

0 in NAT ;

then reconsider zz = 0 as Element of REAL by NUMBERS:19;

consider u1, u2, v1, v2 being Element of REAL such that

A13: 1 = [*u1,u2*] and

A14: ( y = [*v1,v2*] & 1 * y = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] ) by Def4;

A15: u2 = 0 by A13, ARYTM_0:24, Lm2;

then A16: + ((* (u1,v2)),(* (u2,v1))) = * (u1,v2) by ARYTM_0:11, ARYTM_0:12;

A17: u1 = 1 by A13, A15, ARYTM_0:def 5;

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

then A18: opp zz = 0 by ARYTM_0:11;

A19: + ((* (u1,v1)),(opp (* (u2,v2)))) = + (v1,(opp (* (u2,v2)))) by A17, ARYTM_0:19

.= + (v1,(* ((opp u2),v2))) by ARYTM_0:15

.= + (v1,(* (zz,v2))) by A13, A18, ARYTM_0:24, Lm2

.= v1 by ARYTM_0:11, ARYTM_0:12 ;

set z = 0 ;

consider u1, u2, v1, v2 being Element of REAL such that

x " = [*u1,u2*] and

A20: 0 = [*v1,v2*] and

A21: (x ") * 0 = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] by Def4;

v2 = zz by A20, ARYTM_0:24;

then A22: v1 = 0 by A20, ARYTM_0:def 5;

then A23: + ((* (u1,v1)),(opp (* (u2,v2)))) = opp (* (u2,v2)) by ARYTM_0:11, ARYTM_0:12

.= 0 by A18, A20, ARYTM_0:12, ARYTM_0:24 ;

A24: + ((* (u1,v2)),(* (u2,v1))) = + (zz,(* (u2,v1))) by A20, ARYTM_0:12, ARYTM_0:24

.= * (u2,v1) by ARYTM_0:11

.= 0 by A22, ARYTM_0:12 ;

assume A25: x * y = 0 ; :: according to ORDINAL1:def 14 :: thesis: contradiction

A26: ((x ") * x) * y = (x ") * (x * y) by Lm5

.= 0 by A21, A23, A24, A25, ARYTM_0:def 5 ;

((x ") * x) * y = 1 * y by Def6

.= y by A14, A16, A17, A19, ARYTM_0:19 ;

hence contradiction by A26; :: thesis: verum

0 in NAT ;

then reconsider zz = 0 as Element of REAL by NUMBERS:19;

consider u1, u2, v1, v2 being Element of REAL such that

A13: 1 = [*u1,u2*] and

A14: ( y = [*v1,v2*] & 1 * y = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] ) by Def4;

A15: u2 = 0 by A13, ARYTM_0:24, Lm2;

then A16: + ((* (u1,v2)),(* (u2,v1))) = * (u1,v2) by ARYTM_0:11, ARYTM_0:12;

A17: u1 = 1 by A13, A15, ARYTM_0:def 5;

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

then A18: opp zz = 0 by ARYTM_0:11;

A19: + ((* (u1,v1)),(opp (* (u2,v2)))) = + (v1,(opp (* (u2,v2)))) by A17, ARYTM_0:19

.= + (v1,(* ((opp u2),v2))) by ARYTM_0:15

.= + (v1,(* (zz,v2))) by A13, A18, ARYTM_0:24, Lm2

.= v1 by ARYTM_0:11, ARYTM_0:12 ;

set z = 0 ;

consider u1, u2, v1, v2 being Element of REAL such that

x " = [*u1,u2*] and

A20: 0 = [*v1,v2*] and

A21: (x ") * 0 = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] by Def4;

v2 = zz by A20, ARYTM_0:24;

then A22: v1 = 0 by A20, ARYTM_0:def 5;

then A23: + ((* (u1,v1)),(opp (* (u2,v2)))) = opp (* (u2,v2)) by ARYTM_0:11, ARYTM_0:12

.= 0 by A18, A20, ARYTM_0:12, ARYTM_0:24 ;

A24: + ((* (u1,v2)),(* (u2,v1))) = + (zz,(* (u2,v1))) by A20, ARYTM_0:12, ARYTM_0:24

.= * (u2,v1) by ARYTM_0:11

.= 0 by A22, ARYTM_0:12 ;

assume A25: x * y = 0 ; :: according to ORDINAL1:def 14 :: thesis: contradiction

A26: ((x ") * x) * y = (x ") * (x * y) by Lm5

.= 0 by A21, A23, A24, A25, ARYTM_0:def 5 ;

((x ") * x) * y = 1 * y by Def6

.= y by A14, A16, A17, A19, ARYTM_0:19 ;

hence contradiction by A26; :: thesis: verum