let z1, z2 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 z19 = z1, z29 = 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 A3: z1 * z2 = 1. F_Complex ; :: thesis: z1 = z2 "

A4: z2 " = z29 " by A1, Th5;
z19 * z29 = 1r by A3, Def1;
hence z1 = z2 " by A1, A4, Th7, XCMPLX_0:def 7; :: thesis: verum

end;

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

A6: z2 " = z29 " by A1, Th5;
z29 * z19 = 1r by A5, Def1;
hence z1 = z2 " by A1, A6, Th7, XCMPLX_0:def 7; :: thesis: verum

end;

end;