let i be Nat; :: thesis: for f being one-to-one FinSequence st i in dom f holds
(f . i) .. f = i
let f be one-to-one FinSequence; :: thesis: ( i in dom f implies (f . i) .. f = i )
assume A1: i in dom f ; :: thesis: (f . i) .. f = i
then f . i in rng f by FUNCT_1:def 3;
then A2: f just_once_values f . i by FINSEQ_4:8;
then f <- (f . i) = (f . i) .. f by FINSEQ_4:25;
hence (f . i) .. f = i by A1, A2, FINSEQ_4:def 3; :: thesis: verum