let n be Nat; :: thesis: (2 * (n + 1)) choose (n + 1) = 2 * (((2 * n) + 1) choose n)
(((2 * n) + 1) + 1) choose (n + 1) = (((n + n) + 1) choose n) + (((n + n) + 1) choose (n + 1)) by NEWTON:22
.= (((n + 1) + n) choose n) + (((n + 1) + n) choose n) by N20
.= 2 * (((2 * n) + 1) choose n) ;
hence (2 * (n + 1)) choose (n + 1) = 2 * (((2 * n) + 1) choose n) ; :: thesis: verum