let z, z9 be complex number ; :: 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 Th28;
hence z9 = (Re z) + ((- (Im z)) * <i> ) by Th29
.= (Re z) - ((Im z) * <i> ) ;
:: thesis: verum