let z, z' be complex number ; :: thesis: ( z = (Re z') - ((Im z') * <i> ) implies z' = (Re z) - ((Im z) * <i> ) )
assume z = (Re z') - ((Im z') * <i> ) ; :: thesis: z' = (Re z) - ((Im z) * <i> )
then z = (Re z') + ((- (Im z')) * <i> ) ;
then ( Re z = Re z' & - (Im z) = - (- (Im z')) ) by Th28;
hence z' = (Re z) + ((- (Im z)) * <i> ) by Th29
.= (Re z) - ((Im z) * <i> ) ;
:: thesis: verum