let x be Element of F_Complex; :: thesis: ( Im x = 0 implies x = x *' )
reconsider d = x as Element of COMPLEX by COMPLFLD:def 1;
assume Im x = 0 ; :: thesis: x = x *'
hence x = (Re d) + ((- (Im d)) * <i>) by COMPLEX1:13
.= x *' ;
:: thesis: verum