let c1, c2 be complex number ; :: thesis:
thus ( z <> 0 & z * c1 = 1 & z * c2 = 1 implies c1 = c2 ) :: thesis:

proof

assume that
A18: z <> 0 and
A19: z * c1 = 1 and
A20: z * c2 = 1 ; :: thesis:
A21: for z' being complex number st z * z' = 1 holds
z' = [*(* x,(inv (+ (* x,x),(* y,y)))),(* (opp y),(inv (+ (* x,x),(* y,y))))*]

proof

let z' be complex number ; :: thesis:
assume A22: z * z' = 1 ; :: thesis:
consider x1, x2, x', y' being Element of REAL such that
A23: z = [*x1,x2*] and
A24: z' = [*x',y'*] and
A25: 1 = [*(+ (* x1,x'),(opp (* x2,y'))),(+ (* x1,y'),(* x2,x'))*] by A22, Def5;
A26: ( x = x1 & y = x2 ) by A1, A23, ARYTM_0:12;

per cases by A1, A18, ARYTM_0:def 7;

suppose that A27: x = 0 and
A28: y <> 0 ; :: thesis:

+ y,(opp y) = 0 by ARYTM_0:def 4;
then A29: opp y <> 0 by A28, ARYTM_0:13;
A30: * x,y' = 0 by A27, ARYTM_0:14;
* x,x' = 0 by A27, ARYTM_0:14;
then A31: 1 = [*(opp (* y,y')),(+ 0 ,(* y,x'))*] by A25, A26, A30, ARYTM_0:13
.= [*(opp (* y,y')),(* y,x')*] by ARYTM_0:13 ;
A32: 1 = [*j,0 *] by ARYTM_0:def 7;
* (opp y),y' = opp (* y,y') by ARYTM_0:17
.= 1 by A31, A32, ARYTM_0:12 ;
then A33: y' = inv (opp y) by A29, ARYTM_0:def 5;
A34: * x,x = 0 by A27, ARYTM_0:14;
* (opp y),(opp (inv y)) = opp (* y,(opp (inv y))) by ARYTM_0:17
.= opp (opp (* y,(inv y))) by ARYTM_0:17
.= 1 by A28, ARYTM_0:def 5 ;
then A35: inv (opp y) = opp (inv y) by A29, ARYTM_0:def 5;
* y,x' = 0 by A31, A32, ARYTM_0:12;
hence z' = [*0 ,(inv (opp y))*] by A24, A28, A33, ARYTM_0:23
.= [*0 ,(opp (* j,(inv y)))*] by A35, ARYTM_0:21
.= [*0 ,(opp (* (* y,(inv y)),(inv y)))*] by A28, ARYTM_0:def 5
.= [*0 ,(opp (* y,(* (inv y),(inv y))))*] by ARYTM_0:15
.= [*0 ,(* (opp y),(* (inv y),(inv y)))*] by ARYTM_0:17
.= [*0 ,(* (opp y),(inv (* y,y)))*] by ARYTM_0:24
.= [*0 ,(* (opp y),(inv (+ 0 ,(* y,y))))*] by ARYTM_0:13
.= [*(* x,(inv (+ (* x,x),(* y,y)))),(* (opp y),(inv (+ (* x,x),(* y,y))))*] by A27, A34, ARYTM_0:14 ;
:: thesis:

end;

suppose that A36: opp y = 0 and
A37: x <> 0 ; :: thesis:

+ y,(opp y) = 0 by ARYTM_0:def 4;
then A38: y = 0 by A36, ARYTM_0:13;
then A39: * y,x' = 0 by ARYTM_0:14;
opp (* y,y') = * (opp y),y' by ARYTM_0:17
.= 0 by A36, ARYTM_0:14 ;
then A40: 1 = [*(* x,x'),(+ (* x,y'),0 )*] by A25, A26, A39, ARYTM_0:13
.= [*(* x,x'),(* x,y')*] by ARYTM_0:13 ;
A41: 1 = [*j,0 *] by ARYTM_0:def 7;
then * x,x' = 1 by A40, ARYTM_0:12;
then A42: x' = inv x by A37, ARYTM_0:def 5;
* x,y' = 0 by A40, A41, ARYTM_0:12;
then A43: y' = 0 by A37, ARYTM_0:23;
A44: * y,y = 0 by A38, ARYTM_0:14;
x' = * j,(inv x) by A42, ARYTM_0:21
.= * (* x,(inv x)),(inv x) by A37, ARYTM_0:def 5
.= * x,(* (inv x),(inv x)) by ARYTM_0:15
.= * x,(inv (* x,x)) by ARYTM_0:24
.= * x,(inv (+ (* x,x),0 )) by ARYTM_0:13 ;
hence z' = [*(* x,(inv (+ (* x,x),(* y,y)))),(* (opp y),(inv (+ (* x,x),(* y,y))))*] by A24, A36, A43, A44, ARYTM_0:14; :: thesis:

end;

suppose that A45: opp y <> 0 and
A46: x <> 0 ; :: thesis:

A47: now

assume + (* (* x,x),(inv (opp y))),(opp y) = 0 ; :: thesis:
then + (* (* x,x),(inv (opp y))),(* (opp y),j) = 0 by ARYTM_0:21;
then + (* (* x,x),(inv (opp y))),(* (opp y),(* (opp y),(inv (opp y)))) = 0 by A45, ARYTM_0:def 5;
then + (* (* x,x),(inv (opp y))),(* (* (opp y),(opp y)),(inv (opp y))) = 0 by ARYTM_0:15;
then A48: * (inv (opp y)),(+ (* x,x),(* (opp y),(opp y))) = 0 by ARYTM_0:16;
+ (* x,x),(* (opp y),(opp y)) <> 0 by A46, ARYTM_0:19;
then A49: inv (opp y) = 0 by A48, ARYTM_0:23;
* (opp y),(inv (opp y)) = 1 by A45, ARYTM_0:def 5;
hence contradiction by A49, ARYTM_0:14; :: thesis:

end;

reconsider j = 1 as Element of REAL ;
A50: 1 = [*j,0 *] by ARYTM_0:def 7;
then + (* x1,y'),(* x2,x') = 0 by A25, ARYTM_0:12;
then * x,y' = opp (* y,x') by A26, ARYTM_0:def 4;
then * x,y' = * (opp y),x' by ARYTM_0:17;
then A51: x' = * (* x,y'),(inv (opp y)) by A45, ARYTM_0:22
.= * x,(* y',(inv (opp y))) by ARYTM_0:15 ;
then + (* x,(* x,(* y',(inv (opp y))))),(opp (* y,y')) = 1 by A25, A26, A50, ARYTM_0:12;
then + (* (* x,x),(* y',(inv (opp y)))),(opp (* y,y')) = 1 by ARYTM_0:15;
then + (* (* x,x),(* y',(inv (opp y)))),(* (opp y),y') = 1 by ARYTM_0:17;
then + (* y',(* (* x,x),(inv (opp y)))),(* (opp y),y') = 1 by ARYTM_0:15;
then * y',(+ (* (* x,x),(inv (opp y))),(opp y)) = 1 by ARYTM_0:16;
then A52: y' = inv (+ (* (* x,x),(inv (opp y))),(opp y)) by A47, ARYTM_0:def 5;
then A53: x' = * x,(inv (* (+ (* (* x,x),(inv (opp y))),(opp y)),(opp y))) by A51, ARYTM_0:24
.= * x,(inv (+ (* (* (* x,x),(inv (opp y))),(opp y)),(* (opp y),(opp y)))) by ARYTM_0:16
.= * x,(inv (+ (* (* (* x,x),(inv (opp y))),(opp y)),(opp (* y,(opp y))))) by ARYTM_0:17
.= * x,(inv (+ (* (* (* x,x),(inv (opp y))),(opp y)),(opp (opp (* y,y))))) by ARYTM_0:17
.= * x,(inv (+ (* (* x,x),(* (inv (opp y)),(opp y))),(* y,y))) by ARYTM_0:15
.= * x,(inv (+ (* (* x,x),j),(* y,y))) by A45, ARYTM_0:def 5
.= * x,(inv (+ (* x,x),(* y,y))) by ARYTM_0:21 ;
y' = * j,(inv (+ (* (* x,x),(inv (opp y))),(opp y))) by A52, ARYTM_0:21
.= * (* (opp y),(inv (opp y))),(inv (+ (* (* x,x),(inv (opp y))),(opp y))) by A45, ARYTM_0:def 5
.= * (opp y),(* (inv (opp y)),(inv (+ (* (* x,x),(inv (opp y))),(opp y)))) by ARYTM_0:15
.= * (opp y),(inv (* (opp y),(+ (* (* x,x),(inv (opp y))),(opp y)))) by ARYTM_0:24
.= * (opp y),(inv (+ (* (opp y),(* (* x,x),(inv (opp y)))),(* (opp y),(opp y)))) by ARYTM_0:16
.= * (opp y),(inv (+ (* (* x,x),(* (opp y),(inv (opp y)))),(* (opp y),(opp y)))) by ARYTM_0:15
.= * (opp y),(inv (+ (* (* x,x),j),(* (opp y),(opp y)))) by A45, ARYTM_0:def 5
.= * (opp y),(inv (+ (* x,x),(* (opp y),(opp y)))) by ARYTM_0:21
.= * (opp y),(inv (+ (* x,x),(opp (* y,(opp y))))) by ARYTM_0:17
.= * (opp y),(inv (+ (* x,x),(opp (opp (* y,y))))) by ARYTM_0:17
.= * (opp y),(inv (+ (* x,x),(* y,y))) ;
hence z' = [*(* x,(inv (+ (* x,x),(* y,y)))),(* (opp y),(inv (+ (* x,x),(* y,y))))*] by A24, A53; :: thesis:

end;

hence c1 = [*(* x,(inv (+ (* x,x),(* y,y)))),(* (opp y),(inv (+ (* x,x),(* y,y))))*] by A19
.= c2 by A20, A21 ;
:: thesis:

end;

thus ( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 ) ; :: thesis: