theorem Th9: :: CATALAN2:9

for n being Nat
for p being XFinSequence of NAT st p is dominated_by_0 & n <= (len p) - (2 * (Sum p)) holds
p ^ (n --> 1) is dominated_by_0