theorem Th10: :: CATALAN2:10

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