let n, k be Nat; :: thesis: ex p being XFinSequence of NAT st
( Sum p = card (Domin_0 ((((2 * n) + 2) + k),(n + 1))) & dom p = k + 1 & ( for i being Nat st i <= k holds
p . i = card (Domin_0 ((((2 * n) + 1) + i),n)) ) )
defpred S₁[ set , set ] means for j being Nat st $1 = j holds
$2 = card (Domin_0 ((((2 * n) + 1) + j),n));
A1: for i being Nat st i in Segm (k + 1) holds
ex x being Element of NAT st S₁[i,x]

proof

let i be Nat; :: thesis: ( i in Segm (k + 1) implies ex x being Element of NAT st S₁[i,x] )
assume i in Segm (k + 1) ; :: thesis: ex x being Element of NAT st S₁[i,x]
S₁[i, card (Domin_0 ((((2 * n) + 1) + i),n))] ;
hence ex x being Element of NAT st S₁[i,x] ; :: thesis: verum

end;

consider p being XFinSequence of NAT such that
A2: dom p = Segm (k + 1) and
A3: for i being Nat st i in Segm (k + 1) holds
S₁[i,p . i] from STIRL2_1:sch 5(A1);
take p ; :: thesis: ( Sum p = card (Domin_0 ((((2 * n) + 2) + k),(n + 1))) & dom p = k + 1 & ( for i being Nat st i <= k holds
p . i = card (Domin_0 ((((2 * n) + 1) + i),n)) ) )
A4: for i being Nat st i <= k holds
p . i = card (Domin_0 ((((2 * n) + 1) + i),n))

proof

let i be Nat; :: thesis: ( i <= k implies p . i = card (Domin_0 ((((2 * n) + 1) + i),n)) )
assume i <= k ; :: thesis: p . i = card (Domin_0 ((((2 * n) + 1) + i),n))
then i < k + 1 by NAT_1:13;
then i in Segm (k + 1) by NAT_1:44;
hence p . i = card (Domin_0 ((((2 * n) + 1) + i),n)) by A3; :: thesis: verum

end;

now :: thesis: Sum p = card (Domin_0 ((((2 * n) + 2) + k),(n + 1)))

per cases ( n = 0 or n > 0 ) ;

suppose A5: n = 0 ; :: thesis: Sum p = card (Domin_0 ((((2 * n) + 2) + k),(n + 1)))

for x being object st x in dom p holds
p . x = 1

proof

let x be object ; :: thesis: ( x in dom p implies p . x = 1 )
assume A6: x in dom p ; :: thesis: p . x = 1
reconsider i = x as Nat by A6;
p . i = card (Domin_0 ((((2 * n) + 1) + i),n)) by A2, A3, A6;
hence p . x = 1 by A5, Th24; :: thesis: verum

end;

then p = (k + 1) --> 1 by A2, FUNCOP_1:11;
then Sum p = (k + 1) * 1 by AFINSQ_2:58;
hence Sum p = card (Domin_0 ((((2 * n) + 2) + k),(n + 1))) by A5, Th30; :: thesis: verum

end;

suppose n > 0 ; :: thesis: Sum p = card (Domin_0 ((((2 * n) + 2) + k),(n + 1)))

then reconsider n1 = n - 1 as Nat by NAT_1:20;
defpred S₂[ Nat] means for q being XFinSequence of NAT st dom q = $1 + 1 & ( for i being Nat st i <= $1 holds
q . i = card (Domin_0 ((((2 * n) + 1) + i),n)) ) holds
Sum q = card (Domin_0 ((((2 * n) + 2) + $1),(n + 1)));
A7: for j being Nat st S₂[j] holds
S₂[j + 1]

proof

let j be Nat; :: thesis: ( S₂[j] implies S₂[j + 1] )
assume A8: S₂[j] ; :: thesis: S₂[j + 1]
set CH2 = (((2 * n) + 2) + j) choose (n1 + 1);
set CH1 = (((2 * n) + 2) + j) choose (n + 1);
set j1 = j + 1;
let q be XFinSequence of NAT ; :: thesis: ( dom q = (j + 1) + 1 & ( for i being Nat st i <= j + 1 holds
q . i = card (Domin_0 ((((2 * n) + 1) + i),n)) ) implies Sum q = card (Domin_0 ((((2 * n) + 2) + (j + 1)),(n + 1))) )
assume that
A9: dom q = (j + 1) + 1 and
A10: for i being Nat st i <= j + 1 holds
q . i = card (Domin_0 ((((2 * n) + 1) + i),n)) ; :: thesis: Sum q = card (Domin_0 ((((2 * n) + 2) + (j + 1)),(n + 1)))
A11: 2 * (n + 1) <= (2 * (n + 1)) + (j + 1) by NAT_1:11;
j + 1 <= (j + 1) + 1 by NAT_1:11;
then Segm (j + 1) c= Segm ((j + 1) + 1) by NAT_1:39;
then A12: dom (q | (j + 1)) = j + 1 by A9, RELAT_1:62;
A13: for i being Nat st i <= j holds
(q | (j + 1)) . i = card (Domin_0 ((((2 * n) + 1) + i),n))

proof

let i be Nat; :: thesis: ( i <= j implies (q | (j + 1)) . i = card (Domin_0 ((((2 * n) + 1) + i),n)) )
assume i <= j ; :: thesis: (q | (j + 1)) . i = card (Domin_0 ((((2 * n) + 1) + i),n))
then i < j + 1 by NAT_1:13;
then i < len (q | (j + 1)) by A12;
then ( i in dom (q | (j + 1)) & q . i = card (Domin_0 ((((2 * n) + 1) + i),n)) ) by A10, A12, AFINSQ_1:86;
hence (q | (j + 1)) . i = card (Domin_0 ((((2 * n) + 1) + i),n)) by FUNCT_1:47; :: thesis: verum

end;

set CH4 = (((2 * n) + 1) + (j + 1)) choose n1;
set CH3 = (((2 * n) + 1) + (j + 1)) choose n;
A14: ( 2 * n <= (2 * n) + (1 + (j + 1)) & n1 + 1 = n ) by NAT_1:11;
q . (j + 1) = card (Domin_0 ((((2 * n) + 1) + (j + 1)),n)) by A10;
then A15: q . (j + 1) = ((((2 * n) + 1) + (j + 1)) choose n) - ((((2 * n) + 1) + (j + 1)) choose n1) by A14, Th28;
j + 1 < (j + 1) + 1 by NAT_1:13;
then j + 1 < len q by A9;
then j + 1 in dom q by AFINSQ_1:86;
then A16: Sum (q | ((j + 1) + 1)) = (Sum (q | (j + 1))) + (q . (j + 1)) by AFINSQ_2:65;
2 * (n + 1) <= ((2 * n) + 2) + j by NAT_1:11;
then card (Domin_0 ((((2 * n) + 2) + j),(n + 1))) = ((((2 * n) + 2) + j) choose (n + 1)) - ((((2 * n) + 2) + j) choose (n1 + 1)) by Th28;
then Sum (q | (j + 1)) = ((((2 * n) + 2) + j) choose (n + 1)) - ((((2 * n) + 2) + j) choose (n1 + 1)) by A8, A12, A13;
then (Sum (q | (j + 1))) + (q . (j + 1)) = (((((2 * n) + 2) + j) choose (n + 1)) + ((((2 * n) + 2) + j) choose (n1 + 1))) - (((((2 * n) + 1) + (j + 1)) choose n) + ((((2 * n) + 1) + (j + 1)) choose n1)) by A15
.= (((((2 * n) + 2) + j) + 1) choose (n + 1)) - (((((2 * n) + 1) + (j + 1)) choose n) + ((((2 * n) + 1) + (j + 1)) choose n1)) by NEWTON:22
.= ((((2 * n) + 2) + (j + 1)) choose (n + 1)) - ((((2 * n) + 2) + (j + 1)) choose (n1 + 1)) by NEWTON:22
.= card (Domin_0 ((((2 * n) + 2) + (j + 1)),(n + 1))) by A11, Th28 ;
hence Sum q = card (Domin_0 ((((2 * n) + 2) + (j + 1)),(n + 1))) by A9, A16; :: thesis: verum

end;

A17: S₂[ 0 ]

proof

reconsider 2n1 = (2 * n) + 1 as Nat ;
set 2CHn = ((2 * n) + 2) choose n;
set 2CHn91 = ((2 * n) + 2) choose (n + 1);
set CHn91 = 2n1 choose (n + 1);
set CHn1 = 2n1 choose n1;
set CHn = 2n1 choose n;
let q be XFinSequence of NAT ; :: thesis: ( dom q = 0 + 1 & ( for i being Nat st i <= 0 holds
q . i = card (Domin_0 ((((2 * n) + 1) + i),n)) ) implies Sum q = card (Domin_0 ((((2 * n) + 2) + 0),(n + 1))) )
assume ( dom q = 0 + 1 & ( for i being Nat st i <= 0 holds
q . i = card (Domin_0 ((((2 * n) + 1) + i),n)) ) ) ; :: thesis: Sum q = card (Domin_0 ((((2 * n) + 2) + 0),(n + 1)))
then A18: ( q . 0 = card (Domin_0 ((((2 * n) + 1) + 0),n)) & len q = 1 ) ;
A19: (2 * n) + 2 = ((2 * n) + 1) + 1 ;
then A20: ((2 * n) + 2) choose (n + 1) = (2n1 choose (n + 1)) + (2n1 choose n) by NEWTON:22;
n1 + 1 = n ;
then A21: ((2 * n) + 2) choose n = (2n1 choose n) + (2n1 choose n1) by A19, NEWTON:22;
( n <= n + (n + 1) & ((2 * n) + 1) - n = n + 1 ) by NAT_1:11;
then A22: 2n1 choose n = 2n1 choose (n + 1) by NEWTON:20;
2 * (n + 1) = (2 * n) + 2 ;
then A23: card (Domin_0 (((2 * n) + 2),(n + 1))) = (((2 * n) + 2) choose (n + 1)) - (((2 * n) + 2) choose n) by Th28;
( card (Domin_0 (2n1,(n1 + 1))) = (2n1 choose n) - (2n1 choose n1) & Sum <%(q . 0)%> = q . 0 ) by Th28, AFINSQ_2:53, NAT_1:11;
hence Sum q = card (Domin_0 ((((2 * n) + 2) + 0),(n + 1))) by A20, A21, A22, A23, A18, AFINSQ_1:34; :: thesis: verum

end;

for j being Nat holds S₂[j] from NAT_1:sch 2(A17, A7);
hence Sum p = card (Domin_0 ((((2 * n) + 2) + k),(n + 1))) by A2, A4; :: thesis: verum

end;

end;

end;

hence ( Sum p = card (Domin_0 ((((2 * n) + 2) + k),(n + 1))) & dom p = k + 1 & ( for i being Nat st i <= k holds
p . i = card (Domin_0 ((((2 * n) + 1) + i),n)) ) ) by A2, A4; :: thesis: verum