let z be Complex; :: thesis: ( z = z *' implies Im z = 0 )
assume z = z *' ; :: thesis: Im z = 0
then Im z = 0 + (- (Im z)) by COMPLEX1:27;
hence Im z = 0 ; :: thesis: verum