let z be Complex; :: thesis: ( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) )
z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>) by Lm24;
hence ( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) ) by Th12; :: thesis: verum