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