let S be FinSequence; :: thesis: for n being non zero natural number st S is one-to-one & n <= len S holds
(S . n) .. S = n
let n be non zero Nat; :: thesis: ( S is one-to-one & n <= len S implies (S . n) .. S = n )
assume that
A1: S is one-to-one and
A2: n <= len S ; :: thesis: (S . n) .. S = n
set m = (S . n) .. S;
0 + 1 <= n by NAT_1:14;
then A3: n in dom S by A2, FINSEQ_3:27;
then A4: S . n in rng S by FUNCT_1:12;
then A5: S . ((S . n) .. S) = S . n by FINSEQ_4:29;
(S . n) .. S in dom S by A4, FINSEQ_4:30;
hence (S . n) .. S = n by A1, A3, A5, FUNCT_1:def 8; :: thesis: verum