theorem Th40: :: CATALAN2:40

for m, n being Nat holds card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } = card (Domin_0 (n,m))