<%d,d1%> = <%d%> ^ <%d1%> by AFINSQ_1:def 6;
hence <%d,d1%> is XFinSequence of ; :: thesis: verum