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