let x be set ; :: thesis: for n, k being Element of NAT holds
( x in Choose n,k,1,0 iff ex F being XFinSequence of st
( F = x & dom F = n & rng F c= {0 ,1} & Sum F = k ) )
let n, k be Element of NAT ; :: thesis: ( x in Choose n,k,1,0 iff ex F being XFinSequence of 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 st
( F = x & dom F = n & rng F c= {0 ,1} & Sum F = k ) )
:: thesis: ( ex F being XFinSequence of 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 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:7;
rng F is
Subset of
NAT
by A2, XBOOLE_1:1;
then reconsider F =
F as
XFinSequence of
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, Th45;
hence
(
F = x &
dom F = n &
rng F c= {0 ,1} &
Sum F = k )
by A1, A2;
:: thesis: verum
end;
given F being XFinSequence of such that A3:
( F = x & dom F = n & rng F c= {0 ,1} & Sum F = k )
; :: thesis: x in Choose n,k,1,0
1 * (card (F " {1})) = k
by A3, Th45;
then
( card (F " {1}) = k & F is Function of n,{0 ,1} )
by A3, FUNCT_2:4;
hence
x in Choose n,k,1,0
by A3, Def1; :: thesis: verum