theorem Th3: :: CATALAN2:3

for p being XFinSequence of NAT st p is dominated_by_0 holds
p . 0 = 0