let x be set ; :: thesis: for n, k being Nat holds
( x in Choose (n,k,1,0) iff ex F being XFinSequence of NAT st
( F = x & dom F = n & rng F c= {0,1} & Sum F = k ) )
let n, k be Nat; :: thesis: ( x in Choose (n,k,1,0) iff ex F being XFinSequence of NAT st
( F = x & dom F = n & rng F c= {0,1} & Sum F = k ) )
thus ( x in Choose (n,k,1,0) implies ex F being XFinSequence of NAT st
( F = x & dom F = n & rng F c= {0,1} & Sum F = k ) ) :: thesis: ( ex F being XFinSequence of NAT st
( F = x & dom F = n & rng F c= {0,1} & Sum F = k ) implies x in Choose (n,k,1,0) )

proof

assume x in Choose (n,k,1,0) ; :: thesis: ex F being XFinSequence of NAT st
( F = x & dom F = n & rng F c= {0,1} & Sum F = k )
then consider F being Function of n,{0,1} such that
A1: ( x = F & card (F " {1}) = k ) by Def1;
A2: rng F c= {0,1} ;
dom F = n by FUNCT_2:def 1;
then reconsider F = F as XFinSequence by AFINSQ_1:5;
rng F is Subset of NAT by A2, XBOOLE_1:1;
then reconsider F = F as XFinSequence of NAT by RELAT_1:def 19;
take F ; :: thesis: ( F = x & dom F = n & rng F c= {0,1} & Sum F = k )
Sum F = 1 * (card (F " {1})) by A2, AFINSQ_2:68;
hence ( F = x & dom F = n & rng F c= {0,1} & Sum F = k ) by A1, A2, FUNCT_2:def 1; :: thesis: verum

end;

given F being XFinSequence of NAT such that A3: F = x and
A4: ( dom F = n & rng F c= {0,1} & Sum F = k ) ; :: thesis: x in Choose (n,k,1,0)
( 1 * (card (F " {1})) = k & F is Function of n,{0,1} ) by A4, AFINSQ_2:68, FUNCT_2:2;
hence x in Choose (n,k,1,0) by A3, Def1; :: thesis: verum