theorem Th2: :: CATALAN2:2

for k being Nat
for p being XFinSequence of NAT st p is dominated_by_0 holds
2 * (Sum (p | k)) <= k