theorem Th25: :: CATALAN2:25

for p being XFinSequence of NAT
for n being Nat st rng p c= {0,n} holds
ex q being XFinSequence of NAT st
( len p = len q & rng q c= {0,n} & ( for k being Nat st k <= len p holds
(Sum (p | k)) + (Sum (q | k)) = n * k ) & ( for k being Nat st k in len p holds
q . k = n - (p . k) ) )