theorem Th6: :: CATALAN2:6

for n being Nat
for p being XFinSequence of NAT st p is dominated_by_0 holds
p | n is dominated_by_0