let n be Nat; :: thesis: (Newton_Coeff ((2 * n) + 1)) . (n + 1) = (Newton_Coeff ((2 * n) + 1)) . (n + 2)
reconsider k = (2 * n) + 1 as Nat ;
A0: ( (n + 1) + n >= (n + 1) + 0 & n + (n + 1) >= n + 0 ) by XREAL_1:6;
A2: len (Newton_Coeff ((2 * n) + 1)) = ((2 * n) + 1) + 1 by NEWTON:def 5;
( 1 + (n + 1) >= 1 + 0 & (n + 2) + n >= (n + 2) + 0 ) by XREAL_1:6;
then A4: ( n + 2 in dom (Newton_Coeff ((2 * n) + 1)) & n + 1 = (n + 2) - 1 ) by A2, FINSEQ_3:25;
((2 * n) + 1) - n = n + 1 ;
then reconsider l = k - n as Nat ;
(Newton_Coeff ((2 * n) + 1)) . (n + 1) = ((2 * n) + 1) choose n by NCI
.= k choose l by A0, NEWTON:20
.= (Newton_Coeff ((2 * n) + 1)) . (n + 2) by A4, NEWTON:def 5 ;
hence (Newton_Coeff ((2 * n) + 1)) . (n + 1) = (Newton_Coeff ((2 * n) + 1)) . (n + 2) ; :: thesis: verum