theorem Th3: :: FSM_3:3

for k being Nat
for p, q being FinSequence st k in dom p & (len p) + 1 = len q holds
k + 1 in dom q