theorem Th16: :: CATALAN2:16

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