take X = { x where x is n -element XFinSequence of D : verum } ; :: thesis: ( X is Subset of (D ^omega) & ( for x being object holds
( x in X iff x is n -element XFinSequence of D ) ) )
X c= D ^omega

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in D ^omega )
assume y in X ; :: thesis: y in D ^omega
then ex x being n -element XFinSequence of D st y = x ;
hence y in D ^omega by AFINSQ_1:def 7; :: thesis: verum

end;

hence X is Subset of (D ^omega) ; :: thesis: for x being object holds
( x in X iff x is n -element XFinSequence of D )
let x be object ; :: thesis: ( x in X iff x is n -element XFinSequence of D )
thus ( x in X implies x is n -element XFinSequence of D ) :: thesis: ( x is n -element XFinSequence of D implies x in X )

proof

assume x in X ; :: thesis: x is n -element XFinSequence of D
then ex y being n -element XFinSequence of D st x = y ;
hence x is n -element XFinSequence of D ; :: thesis: verum

end;

assume x is n -element XFinSequence of D ; :: thesis: x in X
hence x in X ; :: thesis: verum