let z, z' be complex number ; :: thesis: ( ( z' <> 0 implies z' * z = 1 ) & ( not z' <> 0 implies z = 0 ) implies ( ( z <> 0 implies z * z' = 1 ) & ( not z <> 0 implies z' = 0 ) ) )
assume that
A54: ( z' <> 0 implies z' * z = 1 ) and
A55: ( z' = 0 implies z = 0 ) ; :: thesis: ( ( z <> 0 implies z * z' = 1 ) & ( not z <> 0 implies z' = 0 ) )
thus ( z <> 0 implies z * z' = 1 ) by A54, A55; :: thesis: ( not z <> 0 implies z' = 0 )
assume A56: z = 0 ; :: thesis: z' = 0
assume z' <> 0 ; :: thesis: contradiction
then consider x1, x2, y1, y2 being Element of REAL such that
A57: z = [*x1,x2*] and
z' = [*y1,y2*] and
A58: 1 = [*(+ (* x1,y1),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*] by A54, Def5;
z = [*0 ,0 *] by A56, ARYTM_0:def 7;
then A59: ( x1 = 0 & x2 = 0 ) by A57, ARYTM_0:12;
then A60: * x1,y1 = 0 by ARYTM_0:14;
* x2,y2 = 0 by A59, ARYTM_0:14;
then A61: + (* x1,y1),(opp (* x2,y2)) = 0 by A60, ARYTM_0:def 4;
( * x1,y2 = 0 & * x2,y1 = 0 ) by A59, ARYTM_0:14;
then + (* x1,y2),(* x2,y1) = 0 by ARYTM_0:13;
hence contradiction by A58, A61, ARYTM_0:def 7; :: thesis: verum