theorem Th1: :: CATALAN2:1

for D being set
for n being Nat
for pd being XFinSequence of D ex qd being XFinSequence of D st pd = (pd | n) ^ qd