theorem :: CATALAN2:19

for k being Nat
for p being XFinSequence of NAT st rng p c= {0,1} & (2 * k) + 1 = min* { N where N is Nat : 2 * (Sum (p | N)) > N } holds
p | (2 * k) is dominated_by_0