let z be Element of F_Complex; :: thesis: ( z *' = 0. F_Complex implies z = 0. F_Complex )
assume z *' = 0. F_Complex ; :: thesis: z = 0. F_Complex
then z *' = 0c by Def1;
then z = 0c by COMPLEX1:29;
hence z = 0. F_Complex by Def1; :: thesis: verum