theorem Th14: :: CATALAN2:14

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