let n be Nat; card { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } = (2 * n) choose n
set D = bool ({0,1} ^omega);
set 2n = 2 * n;
defpred S1[ set , set ] means for i being Nat st i = $1 holds
$2 = Domin_0 ((2 * n),i);
set Z = { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } ;
A1:
for k being Nat st k in Segm (n + 1) holds
ex x being Element of bool ({0,1} ^omega) st S1[k,x]
consider r being XFinSequence of bool ({0,1} ^omega) such that
A2:
( dom r = Segm (n + 1) & ( for k being Nat st k in Segm (n + 1) holds
S1[k,r . k] ) )
from STIRL2_1:sch 5(A1);
A3:
{ pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } c= union (rng r)
A8:
union (rng r) c= { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) }
A14:
for i, j being Nat st i in dom r & j in dom r & i <> j holds
r . i misses r . j
proof
let i,
j be
Nat;
( i in dom r & j in dom r & i <> j implies r . i misses r . j )
assume that A15:
i in dom r
and A16:
j in dom r
and A17:
i <> j
;
r . i misses r . j
assume
r . i meets r . j
;
contradiction
then
(r . i) /\ (r . j) <> {}
;
then consider x being
object such that A18:
x in (r . i) /\ (r . j)
by XBOOLE_0:def 1;
A19:
x in r . j
by A18, XBOOLE_0:def 4;
r . j = Domin_0 (
(2 * n),
j)
by A2, A16;
then A20:
ex
q being
XFinSequence of
NAT st
(
q = x &
q is
dominated_by_0 &
dom q = 2
* n &
Sum q = j )
by A19, Def2;
A21:
x in r . i
by A18, XBOOLE_0:def 4;
r . i = Domin_0 (
(2 * n),
i)
by A2, A15;
then
ex
p being
XFinSequence of
NAT st
(
p = x &
p is
dominated_by_0 &
dom p = 2
* n &
Sum p = i )
by A21, Def2;
hence
contradiction
by A17, A20;
verum
end;
A22:
for i being Nat st i in dom r holds
r . i is finite
consider Cardr being XFinSequence of NAT such that
A23:
dom Cardr = dom r
and
A24:
for i being Nat st i in dom Cardr holds
Cardr . i = card (r . i)
and
A25:
card (union (rng r)) = Sum Cardr
by A22, A14, STIRL2_1:66;
A26:
( n < dom Cardr & Cardr | (n + 1) = Cardr )
by A2, A23, NAT_1:13;
defpred S2[ Nat] means ( $1 < len Cardr implies Sum (Cardr | ($1 + 1)) = (2 * n) choose $1 );
A27:
S2[ 0 ]
A34:
for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be
Nat;
( S2[i] implies S2[i + 1] )
assume A35:
S2[
i]
;
S2[i + 1]
set i1 =
i + 1;
assume A36:
i + 1
< len Cardr
;
Sum (Cardr | ((i + 1) + 1)) = (2 * n) choose (i + 1)
then A37:
i + 1
in dom Cardr
by AFINSQ_1:86;
then A38:
(
(Sum (Cardr | (i + 1))) + (Cardr . (i + 1)) = Sum (Cardr | ((i + 1) + 1)) &
Cardr . (i + 1) = card (r . (i + 1)) )
by A24, AFINSQ_2:65;
i + 1
<= n
by A2, A23, A36, NAT_1:13;
then A39:
2
* (i + 1) <= 2
* n
by XREAL_1:64;
r . (i + 1) = Domin_0 (
(2 * n),
(i + 1))
by A2, A23, A37;
then
Sum (Cardr | ((i + 1) + 1)) = ((2 * n) choose i) + (((2 * n) choose (i + 1)) - ((2 * n) choose i))
by A35, A36, A38, A39, Th28, NAT_1:13;
hence
Sum (Cardr | ((i + 1) + 1)) = (2 * n) choose (i + 1)
;
verum
end;
for i being Nat holds S2[i]
from NAT_1:sch 2(A27, A34);
then
Sum Cardr = (2 * n) choose n
by A26;
hence
card { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } = (2 * n) choose n
by A25, A3, A8, XBOOLE_0:def 10; verum