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

(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