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