let z be Complex; :: thesis: ( z *' = 0 implies z = 0 )
assume z *' = 0 ; :: thesis: z = 0
then 0 = (Re z) + ((- (Im z)) * <i>) ;
hence ( Re z = Re 0 & Im z = Im 0 ) by Th12; :: according to COMPLEX1:def 3 :: thesis: verum