let c be Complex; :: thesis: Product <%c%> = c
c in COMPLEX by XCMPLX_0:def 2;
hence Product <%c%> = c by AFINSQ_2:37; :: thesis: verum