theorem Th1: :: REWRITE2:1

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