theorem :: AFINSQ_1:42

for x being object
for D being set holds
( x in D ^omega iff x is XFinSequence of D ) by Def7;