let z, z9 be complex number ; :: 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 ) ) )
assume that
A89: ( z9 <> 0 implies z9 * z = 1 ) and
A90: ( 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 A89, A90; :: thesis: ( not z <> 0 implies z9 = 0 )
assume A91: z = 0 ; :: thesis: z9 = 0
assume z9 <> 0 ; :: thesis: contradiction
then consider x1, x2, y1, y2 being Element of REAL such that
A93: z = [*x1,x2*] and
z9 = [*y1,y2*] and
A94: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by A89, Def5;
A95: z = [*0,0*] by A91, ARYTM_0:def 7;
then A96: x1 = 0 by A93, ARYTM_0:12;
A97: x2 = 0 by A93, A95, ARYTM_0:12;
A98: * (x1,y1) = 0 by A96, ARYTM_0:14;
* (x2,y2) = 0 by A97, ARYTM_0:14;
then A100: + ((* (x1,y1)),(opp (* (x2,y2)))) = 0 by A98, ARYTM_0:def 4;
A101: * (x1,y2) = 0 by A96, ARYTM_0:14;
* (x2,y1) = 0 by A97, ARYTM_0:14;
then + ((* (x1,y2)),(* (x2,y1))) = 0 by A101, ARYTM_0:13;
hence contradiction by A94, A100, ARYTM_0:def 7; :: thesis: verum