theorem Th11: :: CATALAN2:11

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