let x be Element of REAL ; :: thesis: Im (x * <i>) = x
thus Im (x * <i>) = ((Re x) * (Im <i>)) + ((Im x) * (Re <i>)) by Lm17
.= x by Def1, Th7 ; :: thesis: verum