defpred S₁[ set ] means ex p being XFinSequence of st
( p = $1 & p is dominated_by_0 & dom p = n & Sum p = m );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool [:NAT ,NAT :] & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= {0 ,1} ^omega

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in {0 ,1} ^omega )
assume A2: x in X ; :: thesis: x in {0 ,1} ^omega
consider p being XFinSequence of such that
A3: ( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) by A1, A2;
rng p c= {0 ,1} by A3, Def1;
then p is XFinSequence of by RELAT_1:def 19;
hence x in {0 ,1} ^omega by A3, AFINSQ_1:46; :: thesis: verum

end;

then reconsider X = X as Subset of ({0 ,1} ^omega ) ;
take X ; :: thesis: for x being set holds
( x in X iff ex p being XFinSequence of st
( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) )
let x be set ; :: thesis: ( x in X iff ex p being XFinSequence of st
( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) )
thus ( x in X implies S₁[x] ) by A1; :: thesis: ( ex p being XFinSequence of st
( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) implies x in X )
given p being XFinSequence of such that A4: ( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ; :: thesis: x in X
( dom p c= NAT & rng p c= NAT ) by RELAT_1:def 19;
then ( p c= [:(dom p),(rng p):] & [:(dom p),(rng p):] c= [:NAT ,NAT :] ) by RELAT_1:21, ZFMISC_1:119;
then p c= [:NAT ,NAT :] by XBOOLE_1:1;
hence x in X by A1, A4; :: thesis: verum