theorem Th26: :: FINSEQ_5:26

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