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

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