theorem :: CARD_FIN:40

for x being set
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 ) )