theorem Th15: :: CATALAN2:15

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