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