theorem NP1: :: NEWTON07:11

for n being Nat holds (2 * (n + 1)) choose (n + 1) = 2 * (((2 * n) + 1) choose n)