<%d,d1,d2%> = (<%d%> ^ <%d1%>) ^ <%d2%> by AFINSQ_1:def 7;
hence <%d,d1,d2%> is XFinSequence of ; :: thesis: verum