let n be 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 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]
proof
let k be Nat; :: thesis: ( k in Segm (n + 1) implies ex x being Element of bool ({0,1} ^omega) st S1[k,x] )
assume k in Segm (n + 1) ; :: thesis: ex x being Element of bool ({0,1} ^omega) st S1[k,x]
reconsider Z = Domin_0 ((2 * n),k) as Element of bool ({0,1} ^omega) ;
take Z ; :: thesis: S1[k,Z]
thus S1[k,Z] ; :: thesis: verum
end;
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)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } or x in union (rng r) )
assume x in { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } ; :: thesis: x in union (rng r)
then consider pN being Element of NAT ^omega such that
A4: x = pN and
A5: ( dom pN = 2 * n & pN is dominated_by_0 ) ;
pN in Domin_0 ((2 * n),(Sum pN)) by A5, Th20;
then 2 * (Sum pN) <= 2 * n by Th22;
then (1 / 2) * (2 * (Sum pN)) <= (1 / 2) * (2 * n) by XREAL_1:64;
then Sum pN < n + 1 by NAT_1:13;
then A6: Sum pN in Segm (n + 1) by NAT_1:44;
then r . (Sum pN) = Domin_0 ((2 * n),(Sum pN)) by A2;
then A7: pN in r . (Sum pN) by A5, Th20;
r . (Sum pN) in rng r by A2, A6, FUNCT_1:3;
hence x in union (rng r) by A4, A7, TARSKI:def 4; :: thesis: verum
end;
A8: union (rng r) c= { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng r) or x in { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } )
assume x in union (rng r) ; :: thesis: x in { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) }
then consider y being set such that
A9: x in y and
A10: y in rng r by TARSKI:def 4;
consider i being object such that
A11: i in dom r and
A12: y = r . i by A10, FUNCT_1:def 3;
reconsider i = i as Nat by A11;
y = Domin_0 ((2 * n),i) by A2, A11, A12;
then consider p being XFinSequence of NAT such that
A13: ( p = x & p is dominated_by_0 & dom p = 2 * n ) and
Sum p = i by A9, Def2;
p in NAT ^omega by AFINSQ_1:def 7;
hence x in { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } by A13; :: thesis: verum
end;
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; :: thesis: ( 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 ; :: thesis: r . i misses r . j
assume r . i meets r . j ; :: thesis: 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; :: thesis: verum
end;
A22: for i being Nat st i in dom r holds
r . i is finite
proof
let i be Nat; :: thesis: ( i in dom r implies r . i is finite )
assume i in dom r ; :: thesis: r . i is finite
then r . i = Domin_0 ((2 * n),i) by A2;
hence r . i is finite ; :: thesis: verum
end;
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 ]
proof
0 in Segm (n + 1) by NAT_1:44;
then r . 0 = Domin_0 ((2 * n),0) by A2;
then A28: card (r . 0) = 1 by Th24;
A29: 0 in Segm 1 by NAT_1:44;
assume A30: 0 < len Cardr ; :: thesis: Sum (Cardr | (0 + 1)) = (2 * n) choose 0
then 1 <= len Cardr by NAT_1:14;
then A31: Segm 1 c= Segm (len Cardr) by NAT_1:39;
then A32: len (Cardr | 1) = 1 by RELAT_1:62;
dom (Cardr | 1) = 1 by A31, RELAT_1:62;
then (Cardr | 1) . 0 = Cardr . 0 by A29, FUNCT_1:47;
then A33: Cardr | 1 = <%(Cardr . 0)%> by A32, AFINSQ_1:34;
0 in len Cardr by A30, AFINSQ_1:86;
then Cardr . 0 = card (r . 0) by A24;
then Sum (Cardr | 1) = 1 by A33, A28, AFINSQ_2:53;
hence Sum (Cardr | (0 + 1)) = (2 * n) choose 0 by NEWTON:19; :: thesis: verum
end;
A34: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A35: S2[i] ; :: thesis: S2[i + 1]
set i1 = i + 1;
assume A36: i + 1 < len Cardr ; :: thesis: 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) ; :: thesis: 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; :: thesis: verum