reconsider D9OMEGA = D ^omega as functional non empty set ;
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 7; :: thesis: verum