1 in REAL ;
then reconsider j = 1 as complex number by Def2, Lm4;
consider u1, u2, v1, v2 being Element of REAL such that
A12: j = [*u1,u2*] and
A13: ( y = [*v1,v2*] & j * y = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] ) by Def5;
A14: u2 = 0 by A12, ARYTM_0:26;
then A15: + ((* (u1,v2)),(* (u2,v1))) = * (u1,v2) by ARYTM_0:13, ARYTM_0:14;
A16: u1 = 1 by A12, A14, ARYTM_0:def 7;
+ (0,(opp 0)) = 0 by ARYTM_0:def 4;
then A17: opp 0 = 0 by ARYTM_0:13;
A18: + ((* (u1,v1)),(opp (* (u2,v2)))) = + (v1,(opp (* (u2,v2)))) by A16, ARYTM_0:21
.= + (v1,(* ((opp u2),v2))) by ARYTM_0:17
.= + (v1,(* (0,v2))) by A12, A17, ARYTM_0:26
.= v1 by ARYTM_0:13, ARYTM_0:14 ;
0 in REAL ;
then reconsider z = 0 as complex number by Def2, Lm4;
consider u1, u2, v1, v2 being Element of REAL such that
x " = [*u1,u2*] and
A19: z = [*v1,v2*] and
A20: (x ") * z = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] by Def5;
v2 = 0 by A19, ARYTM_0:26;
then A21: v1 = 0 by A19, ARYTM_0:def 7;
then A22: + ((* (u1,v1)),(opp (* (u2,v2)))) = opp (* (u2,v2)) by ARYTM_0:13, ARYTM_0:14
.= 0 by A17, A19, ARYTM_0:14, ARYTM_0:26 ;
A23: + ((* (u1,v2)),(* (u2,v1))) = + (0,(* (u2,v1))) by A19, ARYTM_0:14, ARYTM_0:26
.= * (u2,v1) by ARYTM_0:13
.= 0 by A21, ARYTM_0:14 ;
assume A24: x * y = 0 ; :: according to XCMPLX_0:def 3 :: thesis: contradiction
A25: ((x ") * x) * y = (x ") * (x * y) by Lm3
.= 0 by A20, A22, A23, A24, ARYTM_0:def 7 ;
((x ") * x) * y = j * y by Def7
.= y by A13, A15, A16, A18, ARYTM_0:21 ;
hence contradiction by A25; :: thesis: verum