defpred S1[ object ] means ex p being XFinSequence of NAT st
( p = $1 & p is dominated_by_0 & dom p = n & Sum p = m );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in bool [:NAT,NAT:] & S1[x] ) ) from XBOOLE_0:sch 1();
 X c= {0,1} ^omega
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in {0,1} ^omega )
assume x in X ; :: thesis: x in {0,1} ^omega
then consider p being XFinSequence of NAT such that
A2: p = x and
A3: p is dominated_by_0 and
dom p = n and
Sum p = m by A1;
rng p c= {0,1} by A3;
then p is XFinSequence of {0,1} by RELAT_1:def 19;
hence x in {0,1} ^omega by A2, AFINSQ_1:42; :: 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 NAT 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 NAT st
( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) )
thus ( x in X implies S1[x] ) by A1; :: thesis: ( ex p being XFinSequence of NAT st
( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) implies x in X )
given p being XFinSequence of NAT such that A4: ( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ; :: thesis: x in X
( p c= [:(dom p),(rng p):] & [:(dom p),(rng p):] c= [:NAT,NAT:] ) by RELAT_1:7, ZFMISC_1:96;
then p c= [:NAT,NAT:] ;
hence x in X by A1, A4; :: thesis: verum