theorem :: CATALAN2:41

for n, m being Nat st 2 * m <= n holds
ex CardF being XFinSequence of NAT st
( card (Domin_0 (n,m)) = (Sum CardF) + (card (Domin_0 ((n -' 1),m))) & dom CardF = m & ( for j being Nat st j < m holds
CardF . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1))))) ) )