1 in REAL ;
then reconsider j = 1 as complex number by Def2, Lm4;
consider u1, u2, v1, v2 being Element of REAL such that
A21: j = [*u1,u2*] and
A22: ( y = [*v1,v2*] & j * y = [*(+ (* u1,v1),(opp (* u2,v2))),(+ (* u1,v2),(* u2,v1))*] ) by Def5;
A23: u2 = 0 by A21, ARYTM_0:26;
then A24: + (* u1,v2),(* u2,v1) = * u1,v2 by ARYTM_0:13, ARYTM_0:14;
A25: u1 = 1 by A21, A23, ARYTM_0:def 7;
+ 0 ,(opp 0 ) = 0 by ARYTM_0:def 4;
then A27: opp 0 = 0 by ARYTM_0:13;
A28: + (* u1,v1),(opp (* u2,v2)) = + v1,(opp (* u2,v2)) by A25, ARYTM_0:21
.= + v1,(* (opp u2),v2) by ARYTM_0:17
.= + v1,(* 0 ,v2) by A21, A27, 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
A30: z = [*v1,v2*] and
A31: (x " ) * z = [*(+ (* u1,v1),(opp (* u2,v2))),(+ (* u1,v2),(* u2,v1))*] by Def5;
v2 = 0 by A30, ARYTM_0:26;
then A33: v1 = 0 by A30, ARYTM_0:def 7;
then A34: + (* u1,v1),(opp (* u2,v2)) = opp (* u2,v2) by ARYTM_0:13, ARYTM_0:14
.= 0 by A27, A30, ARYTM_0:14, ARYTM_0:26 ;
A35: + (* u1,v2),(* u2,v1) = + 0 ,(* u2,v1) by A30, ARYTM_0:14, ARYTM_0:26
.= * u2,v1 by ARYTM_0:13
.= 0 by A33, ARYTM_0:14 ;
assume A36: x * y = 0 ; :: according to XCMPLX_0:def 3 :: thesis: contradiction
A37: ((x " ) * x) * y = (x " ) * (x * y) by Lm3
.= 0 by A31, A34, A35, A36, ARYTM_0:def 7 ;
((x " ) * x) * y = j * y by Def7
.= y by A22, A24, A25, A28, ARYTM_0:21 ;
hence contradiction by A37; :: thesis: verum