a <> (Re a) + (0 * <i>) ;
hence not Im a is zero by COMPLEX1:13; :: thesis: verum