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

proof

assume that
A29: z <> 0 and
A30: z * c1 = 1 and
A31: z * c2 = 1 ; :: thesis:
A32: for z9 being complex number st z * z9 = 1 holds
z9 = [*(* x,(inv (+ (* x,x),(* y,y)))),(* (opp y),(inv (+ (* x,x),(* y,y))))*]

proof

let z9 be complex number ; :: thesis:
assume A33: z * z9 = 1 ; :: thesis:
consider x1, x2, x9, y9 being Element of REAL such that
A34: z = [*x1,x2*] and
A35: z9 = [*x9,y9*] and
A36: 1 = [*(+ (* x1,x9),(opp (* x2,y9))),(+ (* x1,y9),(* x2,x9))*] by A33, Def5;
A37: ( x = x1 & y = x2 ) by A2, A34, ARYTM_0:12;

per cases by A2, A29, ARYTM_0:def 7;

suppose that A38: x = 0 and
A39: y <> 0 ; :: thesis:

A40: + y,(opp y) = 0 by ARYTM_0:def 4;
A41: opp y <> 0 by A39, A40, ARYTM_0:13;
A42: ( * x,y9 = 0 & * x,x9 = 0 ) by A38, ARYTM_0:14;
A43: 1 = [*(opp (* y,y9)),(+ 0 ,(* y,x9))*] by A36, A37, A42, ARYTM_0:13
.= [*(opp (* y,y9)),(* y,x9)*] by ARYTM_0:13 ;
A44: 1 = [*j,0 *] by ARYTM_0:def 7;
A45: * (opp y),y9 = opp (* y,y9) by ARYTM_0:17
.= 1 by A43, A44, ARYTM_0:12 ;
A46: y9 = inv (opp y) by A41, A45, ARYTM_0:def 5;
A47: * x,x = 0 by A38, ARYTM_0:14;
A48: * (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 A39, ARYTM_0:def 5 ;
A49: inv (opp y) = opp (inv y) by A41, A48, ARYTM_0:def 5;
A50: * y,x9 = 0 by A43, A44, ARYTM_0:12;
thus z9 = [*0 ,(inv (opp y))*] by A35, A39, A46, A50, ARYTM_0:23
.= [*0 ,(opp (* j,(inv y)))*] by A49, ARYTM_0:21
.= [*0 ,(opp (* (* y,(inv y)),(inv y)))*] by A39, 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 A38, A47, ARYTM_0:14 ; :: thesis:

end;

suppose that A51: opp y = 0 and
A52: x <> 0 ; :: thesis:

A53: + y,(opp y) = 0 by ARYTM_0:def 4;
A54: y = 0 by A51, A53, ARYTM_0:13;
A55: * y,x9 = 0 by A54, ARYTM_0:14;
A56: opp (* y,y9) = * (opp y),y9 by ARYTM_0:17
.= 0 by A51, ARYTM_0:14 ;
A57: 1 = [*(* x,x9),(+ (* x,y9),0 )*] by A36, A37, A55, A56, ARYTM_0:13
.= [*(* x,x9),(* x,y9)*] by ARYTM_0:13 ;
A58: 1 = [*j,0 *] by ARYTM_0:def 7;
A59: * x,x9 = 1 by A57, A58, ARYTM_0:12;
A60: x9 = inv x by A52, A59, ARYTM_0:def 5;
A61: * x,y9 = 0 by A57, A58, ARYTM_0:12;
A62: y9 = 0 by A52, A61, ARYTM_0:23;
A63: * y,y = 0 by A54, ARYTM_0:14;
A64: x9 = * j,(inv x) by A60, ARYTM_0:21
.= * (* x,(inv x)),(inv x) by A52, 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 ;
thus z9 = [*(* x,(inv (+ (* x,x),(* y,y)))),(* (opp y),(inv (+ (* x,x),(* y,y))))*] by A35, A51, A62, A63, A64, ARYTM_0:14; :: thesis:

end;

suppose that A65: opp y <> 0 and
A66: x <> 0 ; :: thesis:

A67: now

assume A68: + (* (* x,x),(inv (opp y))),(opp y) = 0 ; :: thesis:
A69: + (* (* x,x),(inv (opp y))),(* (opp y),j) = 0 by A68, ARYTM_0:21;
A70: + (* (* x,x),(inv (opp y))),(* (opp y),(* (opp y),(inv (opp y)))) = 0 by A65, A69, ARYTM_0:def 5;
A71: + (* (* x,x),(inv (opp y))),(* (* (opp y),(opp y)),(inv (opp y))) = 0 by A70, ARYTM_0:15;
A72: * (inv (opp y)),(+ (* x,x),(* (opp y),(opp y))) = 0 by A71, ARYTM_0:16;
A73: + (* x,x),(* (opp y),(opp y)) <> 0 by A66, ARYTM_0:19;
A74: inv (opp y) = 0 by A72, A73, ARYTM_0:23;
A75: * (opp y),(inv (opp y)) = 1 by A65, ARYTM_0:def 5;
thus contradiction by A74, A75, ARYTM_0:14; :: thesis:

end;

reconsider j = 1 as Element of REAL ;
A76: 1 = [*j,0 *] by ARYTM_0:def 7;
A77: + (* x1,y9),(* x2,x9) = 0 by A36, A76, ARYTM_0:12;
A78: * x,y9 = opp (* y,x9) by A37, A77, ARYTM_0:def 4;
A79: * x,y9 = * (opp y),x9 by A78, ARYTM_0:17;
A80: x9 = * (* x,y9),(inv (opp y)) by A65, A79, ARYTM_0:22
.= * x,(* y9,(inv (opp y))) by ARYTM_0:15 ;
A81: + (* x,(* x,(* y9,(inv (opp y))))),(opp (* y,y9)) = 1 by A36, A37, A76, A80, ARYTM_0:12;
A82: + (* (* x,x),(* y9,(inv (opp y)))),(opp (* y,y9)) = 1 by A81, ARYTM_0:15;
A83: + (* (* x,x),(* y9,(inv (opp y)))),(* (opp y),y9) = 1 by A82, ARYTM_0:17;
A84: + (* y9,(* (* x,x),(inv (opp y)))),(* (opp y),y9) = 1 by A83, ARYTM_0:15;
A85: * y9,(+ (* (* x,x),(inv (opp y))),(opp y)) = 1 by A84, ARYTM_0:16;
A86: y9 = inv (+ (* (* x,x),(inv (opp y))),(opp y)) by A67, A85, ARYTM_0:def 5;
A87: x9 = * x,(inv (* (+ (* (* x,x),(inv (opp y))),(opp y)),(opp y))) by A80, A86, 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 A65, ARYTM_0:def 5
.= * x,(inv (+ (* x,x),(* y,y))) by ARYTM_0:21 ;
A88: y9 = * j,(inv (+ (* (* x,x),(inv (opp y))),(opp y))) by A86, ARYTM_0:21
.= * (* (opp y),(inv (opp y))),(inv (+ (* (* x,x),(inv (opp y))),(opp y))) by A65, 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 A65, 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))) ;
thus z9 = [*(* x,(inv (+ (* x,x),(* y,y)))),(* (opp y),(inv (+ (* x,x),(* y,y))))*] by A35, A87, A88; :: thesis:

end;

thus c1 = [*(* x,(inv (+ (* x,x),(* y,y)))),(* (opp y),(inv (+ (* x,x),(* y,y))))*] by A30, A32
.= c2 by A31, A32 ; :: thesis:

end;

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