let x be Real; :: thesis: Im (x * <i>) = x
thus Im (x * <i>) = ((Re x) * (Im <i>)) + ((Im x) * (Re <i>)) by Lm17
.= x by Def2, Th17 ; :: thesis: verum