<%c1,c2%> = <%c1%> ^ <%c2%> by AFINSQ_1:def 5;
hence <%c1,c2%> is Cardinal-yielding ; :: thesis: verum