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