x + (y * <i>) in COMPLEX by XCMPLX_0:def 2;
hence x + (y * <i>) is Element of F_Complex by COMPLFLD:def 1; :: thesis: verum