theorem Th36: :: CATALAN2:36

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