let z, z9 be Complex; :: thesis: ( ( z9 <> 0 implies z9 * z = 1 ) & ( not z9 <> 0 implies z = 0 ) implies ( ( z <> 0 implies z * z9 = 1 ) & ( not z <> 0 implies z9 = 0 ) ) )

0 in NAT ;

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

assume that

A54: ( z9 <> 0 implies z9 * z = 1 ) and

A55: ( z9 = 0 implies z = 0 ) ; :: thesis: ( ( z <> 0 implies z * z9 = 1 ) & ( not z <> 0 implies z9 = 0 ) )

thus ( z <> 0 implies z * z9 = 1 ) by A54, A55; :: thesis: ( not z <> 0 implies z9 = 0 )

assume A56: z = 0 ; :: thesis: z9 = 0

assume z9 <> 0 ; :: thesis: contradiction

then consider x1, x2, y1, y2 being Element of REAL such that

A57: z = [*x1,x2*] and

z9 = [*y1,y2*] and

A58: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by A54, Def4;

A59: z = [*zz,zz*] by A56, ARYTM_0:def 5;

then A60: x1 = 0 by A57, ARYTM_0:10;

A61: x2 = 0 by A57, A59, ARYTM_0:10;

A62: * (x1,y1) = 0 by A60, ARYTM_0:12;

* (x2,y2) = 0 by A61, ARYTM_0:12;

then A63: + ((* (x1,y1)),(opp (* (x2,y2)))) = 0 by A62, ARYTM_0:def 3;

A64: * (x1,y2) = 0 by A60, ARYTM_0:12;

* (x2,y1) = 0 by A61, ARYTM_0:12;

then + ((* (x1,y2)),(* (x2,y1))) = 0 by A64, ARYTM_0:11;

hence contradiction by A58, A63, ARYTM_0:def 5; :: thesis: verum

0 in NAT ;

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

assume that

A54: ( z9 <> 0 implies z9 * z = 1 ) and

A55: ( z9 = 0 implies z = 0 ) ; :: thesis: ( ( z <> 0 implies z * z9 = 1 ) & ( not z <> 0 implies z9 = 0 ) )

thus ( z <> 0 implies z * z9 = 1 ) by A54, A55; :: thesis: ( not z <> 0 implies z9 = 0 )

assume A56: z = 0 ; :: thesis: z9 = 0

assume z9 <> 0 ; :: thesis: contradiction

then consider x1, x2, y1, y2 being Element of REAL such that

A57: z = [*x1,x2*] and

z9 = [*y1,y2*] and

A58: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by A54, Def4;

A59: z = [*zz,zz*] by A56, ARYTM_0:def 5;

then A60: x1 = 0 by A57, ARYTM_0:10;

A61: x2 = 0 by A57, A59, ARYTM_0:10;

A62: * (x1,y1) = 0 by A60, ARYTM_0:12;

* (x2,y2) = 0 by A61, ARYTM_0:12;

then A63: + ((* (x1,y1)),(opp (* (x2,y2)))) = 0 by A62, ARYTM_0:def 3;

A64: * (x1,y2) = 0 by A60, ARYTM_0:12;

* (x2,y1) = 0 by A61, ARYTM_0:12;

then + ((* (x1,y2)),(* (x2,y1))) = 0 by A64, ARYTM_0:11;

hence contradiction by A58, A63, ARYTM_0:def 5; :: thesis: verum