reconsider D9OMEGA = D ^omega as non empty functional set by Lm5;
take D9OMEGA ; :: thesis: for x being set st x in D9OMEGA holds
x is XFinSequence of
thus for x being set st x in D9OMEGA holds
x is XFinSequence of by AFINSQ_1:def 8; :: thesis: verum