let D be non empty set ; :: thesis: for f being non empty one-to-one FinSequence of D holds (f /. (len f)) .. f = len f
let f be non empty one-to-one FinSequence of D; :: thesis: (f /. (len f)) .. f = len f
A1: len f in dom f by FINSEQ_5:6;
A2: 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 that
A3: 1 <= i and
A4: i < len f ; :: thesis: f . i <> f . (len f)
i in dom f by A3, A4, FINSEQ_3:25;
hence f . i <> f . (len f) by A1, A4, FUNCT_1:def 4; :: thesis: verum

end;

f /. (len f) = f . (len f) by A1, PARTFUN1:def 6;
hence (f /. (len f)) .. f = len f by A1, A2, FINSEQ_6:2; :: thesis: verum