theorem Th39: :: CATALAN2:39

for n being Nat st n > 0 holds
ex Catal being XFinSequence of NAT st
( Sum Catal = Catalan (n + 1) & dom Catal = n & ( for j being Nat st j < n holds
Catal . j = (Catalan (j + 1)) * (Catalan (n -' j)) ) )