theorem Th3: :: REWRITE3:3

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