theorem Th3: :: REVROT_1:3

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