A1: D ^omega is functional by Lm5;
for x being set st x in D ^omega holds
x is XFinSequence of by AFINSQ_1:def 8;
hence D ^omega is OMEGA of D by A1, Def3; :: thesis: verum