:: deftheorem Def7 defines ^omega AFINSQ_1:def 7 :
for D, b₂ being set holds
( b₂ = D ^omega iff for x being object holds
( x in b₂ iff x is XFinSequence of D ) );