let z, z9 be Complex; :: thesis: ( z = (Re z9) - ((Im z9) * <i>) implies z9 = (Re z) - ((Im z) * <i>) )
assume z = (Re z9) - ((Im z9) * <i>) ; :: thesis: z9 = (Re z) - ((Im z) * <i>)
then z = (Re z9) + ((- (Im z9)) * <i>) ;
then ( Re z = Re z9 & - (Im z) = - (- (Im z9)) ) by Th12;
hence z9 = (Re z) + ((- (Im z)) * <i>) by Th13
.= (Re z) - ((Im z) * <i>) ;
:: thesis: verum