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