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