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