let D be non empty set ; :: thesis: for f being non empty FinSequence of D holds f /. (len f) in rng f
let f be non empty FinSequence of D; :: thesis: f /. (len f) in rng f
len f in dom f by FINSEQ_5:6;
hence f /. (len f) in rng f by PARTFUN2:2; :: thesis: verum