let a be non zero Real; :: thesis: for a1 being Complex st a * a1 is Real holds
a1 is Real
let a1 be Complex; :: thesis: ( a * a1 is Real implies a1 is Real )
Im (a1 * a) = ((Re a1) * (Im a)) + ((Re a) * (Im a1)) by COMPLEX1:9
.= ((Re a1) * 0) + (a * (Im a1)) ;
hence ( a * a1 is Real implies a1 is Real ) ; :: thesis: verum