let x be 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 ) )
let n, k be Nat; ( 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 ) )
( 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)
;
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
;
( 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;
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 )
; 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; verum