let z be complex number ; :: thesis: ( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) )
z in COMPLEX by XCMPLX_0:def 2;
then z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>) by Def13;
hence ( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) ) by Th28; :: thesis: verum