theorem Th1: :: TAXONOM1:1

for p being FinSequence
for k being Nat st k + 1 in dom p & not k in dom p holds
k = 0