let n be Nat; :: thesis:
set D = bool ({0,1} ^omega);
set 2n = 2 * n;
defpred S₁[ 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 S₁[k,x]

let k be Nat; :: thesis:
assume k in Segm (n + 1) ; :: thesis:
reconsider Z = Domin_0 ((2 * n),k) as Element of bool ({0,1} ^omega) ;
take Z ; :: thesis:
thus S₁[k,Z] ; :: thesis:

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
S₁[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)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } ; :: thesis:
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:

end;

A8: union (rng r) c= { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) }

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union (rng r) ; :: thesis:
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:

end;

A14: for i, j being Nat st i in dom r & j in dom r & i <> j holds
r . i misses r . j

end;

let i be Nat; :: thesis:
assume i in dom r ; :: thesis:
then r . i = Domin_0 ((2 * n),i) by A2;
hence r . i is finite ; :: thesis:

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 S₂[ Nat] means ( $1 < len Cardr implies Sum (Cardr | ($1 + 1)) = (2 * n) choose $1 );
A27: S₂[ 0 ]

end;

A34: for i being Nat st S₂[i] holds
S₂[i + 1]

let i be Nat; :: thesis:
assume A35: S₂[i] ; :: thesis:
set i1 = i + 1;
assume A36: i + 1 < len Cardr ; :: thesis:
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:

end;

for i being Nat holds S₂[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: