theorem Th39: :: FINSEQ_5:39

for i being Nat
for D being non empty set
for f being FinSequence of D st i in dom f holds
(f /. i) .. f <= i