let D be non empty set ; :: thesis: for f being one-to-one non empty FinSequence of D holds (f /. (len f)) .. f = len f
let f be one-to-one non empty FinSequence of D; :: thesis: (f /. (len f)) .. f = len f
A1: len f in dom f by FINSEQ_5:6;
then A2: f /. (len f) = f . (len f) by PARTFUN1:def 8;
for i being Nat st 1 <= i & i < len f holds
f . i <> f . (len f)

proof

let i be Nat; :: thesis: ( 1 <= i & i < len f implies f . i <> f . (len f) )
assume A3: ( 1 <= i & i < len f ) ; :: thesis: f . i <> f . (len f)
i in dom f by A3, FINSEQ_3:27;
hence f . i <> f . (len f) by A1, A3, FUNCT_1:def 8; :: thesis: verum

end;

hence (f /. (len f)) .. f = len f by A1, A2, FINSEQ_6:4; :: thesis: verum