let a be Real; :: thesis: Re (a * <i>) = 0
thus Re (a * <i>) = ((Re a) * (Re <i>)) - ((Im a) * (Im <i>)) by Th9
.= ((Re a) * 0) - (0 * (Im <i>)) by Th7
.= 0 ; :: thesis: verum