theorem Th3: :: FINSEQ_6:168

for D being non empty set
for f being non empty FinSequence of D holds f /. (len f) in rng f