let n be Element of NAT ; :: thesis: card { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } = (2 * n) choose n
set 2n = 2 * n;
defpred S1[ set , set ] means for i being Element of NAT st i = $1 holds
$2 = Domin_0 (2 * n),i;
set D = bool ({0 ,1} ^omega );
A1:
for k being Element of NAT st k in n + 1 holds
ex x being Element of bool ({0 ,1} ^omega ) st S1[k,x]
consider r being XFinSequence of such that
A2:
( dom r = n + 1 & ( for k being Element of NAT st k in n + 1 holds
S1[k,r . k] ) )
from STIRL2_1:sch 6(A1);
A3:
for i being Element of NAT st i in dom r holds
r . i is finite
A5:
for i, j being Element of NAT st i in dom r & j in dom r & i <> j holds
r . i misses r . j
proof
let i,
j be
Element of
NAT ;
:: thesis: ( i in dom r & j in dom r & i <> j implies r . i misses r . j )
assume A6:
(
i in dom r &
j in dom r &
i <> j )
;
:: thesis: r . i misses r . j
assume
r . i meets r . j
;
:: thesis: contradiction
then
(r . i) /\ (r . j) <> {}
by XBOOLE_0:def 7;
then consider x being
set such that A7:
x in (r . i) /\ (r . j)
by XBOOLE_0:def 1;
(
r . i = Domin_0 (2 * n),
i &
x in r . i )
by A2, A6, A7, XBOOLE_0:def 4;
then consider p being
XFinSequence of
such that A8:
(
p = x &
p is
dominated_by_0 &
dom p = 2
* n &
Sum p = i )
by Def2;
(
r . j = Domin_0 (2 * n),
j &
x in r . j )
by A2, A6, A7, XBOOLE_0:def 4;
then
ex
q being
XFinSequence of st
(
q = x &
q is
dominated_by_0 &
dom q = 2
* n &
Sum q = j )
by Def2;
hence
contradiction
by A6, A8;
:: thesis: verum
end;
consider Cardr being XFinSequence of such that
A9:
dom Cardr = dom r
and
A10:
for i being Element of NAT st i in dom Cardr holds
Cardr . i = card (r . i)
and
A11:
card (union (rng r)) = Sum Cardr
from STIRL2_1:sch 7(A3, A5);
defpred S2[ Element of NAT ] means ( $1 < dom Cardr implies Sum (Cardr | ($1 + 1)) = (2 * n) choose $1 );
A12:
S2[ 0 ]
A15:
for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be
Element of
NAT ;
:: thesis: ( S2[i] implies S2[i + 1] )
assume A16:
S2[
i]
;
:: thesis: S2[i + 1]
set i1 =
i + 1;
assume A17:
i + 1
< dom Cardr
;
:: thesis: Sum (Cardr | ((i + 1) + 1)) = (2 * n) choose (i + 1)
then
i + 1
in dom Cardr
by NAT_1:45;
then A18:
(
(Sum (Cardr | (i + 1))) + (Cardr . (i + 1)) = Sum (Cardr | ((i + 1) + 1)) &
Cardr . (i + 1) = card (r . (i + 1)) &
r . (i + 1) = Domin_0 (2 * n),
(i + 1) )
by A2, A9, A10, CARD_FIN:44;
i + 1
<= n
by A2, A9, A17, NAT_1:13;
then
2
* (i + 1) <= 2
* n
by XREAL_1:66;
then
Sum (Cardr | ((i + 1) + 1)) = ((2 * n) choose i) + (((2 * n) choose (i + 1)) - ((2 * n) choose i))
by A16, A17, A18, Th32, NAT_1:13;
hence
Sum (Cardr | ((i + 1) + 1)) = (2 * n) choose (i + 1)
;
:: thesis: verum
end;
A19:
for i being Element of NAT holds S2[i]
from NAT_1:sch 1(A12, A15);
( n < dom Cardr & Cardr | (n + 1) = Cardr )
by A2, A9, NAT_1:13, RELAT_1:98;
then A20:
Sum Cardr = (2 * n) choose n
by A19;
set Z = { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } ;
A21:
{ pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } c= union (rng r)
union (rng r) c= { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) }
hence
card { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } = (2 * n) choose n
by A11, A20, A21, XBOOLE_0:def 10; :: thesis: verum