theorem :: COMPLEX1:85

for z being Complex holds z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>) by Lm24;