theorem Th17: :: CATALAN2:17

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