let z2, z1 be Element of F_Complex ; :: thesis: ( z2 <> 0. F_Complex & ( z1 * z2 = 1. F_Complex or z2 * z1 = 1. F_Complex ) implies z1 = z2 " )
reconsider z1' = z1, z2' = z2 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; :: thesis: ( ( not z1 * z2 = 1. F_Complex & not z2 * z1 = 1. F_Complex ) or z1 = z2 " )
assume A2: ( z1 * z2 = 1. F_Complex or z2 * z1 = 1. F_Complex ) ; :: thesis: z1 = z2 "

per cases ( z1 * z2 = 1. F_Complex or z2 * z1 = 1. F_Complex ) by A2;

suppose z1 * z2 = 1. F_Complex ; :: thesis: z1 = z2 "

then A3: z1' * z2' = 1r by Def1;
z2 " = z2' " by A1, Th7;
hence z1 = z2 " by A1, A3, Th9, XCMPLX_0:def 7; :: thesis: verum

end;

suppose z2 * z1 = 1. F_Complex ; :: thesis: z1 = z2 "

then A4: z2' * z1' = 1r by Def1;
z2 " = z2' " by A1, Th7;
hence z1 = z2 " by A1, A4, Th9, XCMPLX_0:def 7; :: thesis: verum

end;

end;