c in COMPLEX by XCMPLX_0:def 2;
hence XProduct <%c%> = c by AFINSQ_2:37; :: thesis: verum