theorem Th26: :: FINSEQ_5:26

for i, n being Nat
for f being FinSequence st i in dom (f /^ n) holds
n + i in dom f