theorem :: CATALAN2:35

for n being Nat holds card { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } = (2 * n) choose n