let S be FinSequence; :: thesis: for n being non zero Nat 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:25;
then A4: S . n in rng S by FUNCT_1:3;
then A5: S . ((S . n) .. S) = S . n by FINSEQ_4:19;
(S . n) .. S in dom S by A4, FINSEQ_4:20;
hence (S . n) .. S = n by A1, A3, A5, FUNCT_1:def 4; :: thesis: verum