( D ^omega is functional & ( for x being set st x in D ^omega holds
x is XFinSequence of D ) ) by AFINSQ_1:def 7;
hence D ^omega is OMEGA of D by Def3; :: thesis: verum