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