let k be Nat; :: thesis: for f being FinSequence st k in dom f & ( for i being Nat st 1 <= i & i < k holds

f . i <> f . k ) holds

(f . k) .. f = k

let f be FinSequence; :: thesis: ( k in dom f & ( for i being Nat st 1 <= i & i < k holds

f . i <> f . k ) implies (f . k) .. f = k )

assume that

A1: k in dom f and

A2: for i being Nat st 1 <= i & i < k holds

f . i <> f . k ; :: thesis: (f . k) .. f = k

assume A3: (f . k) .. f <> k ; :: thesis: contradiction

(f . k) .. f <= k by A1, FINSEQ_4:24;

then A4: (f . k) .. f < k by A3, XXREAL_0:1;

A5: f . k in rng f by A1, FUNCT_1:def 3;

then f . ((f . k) .. f) = f . k by FINSEQ_4:19;

hence contradiction by A2, A5, A4, FINSEQ_4:21; :: thesis: verum

f . i <> f . k ) holds

(f . k) .. f = k

let f be FinSequence; :: thesis: ( k in dom f & ( for i being Nat st 1 <= i & i < k holds

f . i <> f . k ) implies (f . k) .. f = k )

assume that

A1: k in dom f and

A2: for i being Nat st 1 <= i & i < k holds

f . i <> f . k ; :: thesis: (f . k) .. f = k

assume A3: (f . k) .. f <> k ; :: thesis: contradiction

(f . k) .. f <= k by A1, FINSEQ_4:24;

then A4: (f . k) .. f < k by A3, XXREAL_0:1;

A5: f . k in rng f by A1, FUNCT_1:def 3;

then f . ((f . k) .. f) = f . k by FINSEQ_4:19;

hence contradiction by A2, A5, A4, FINSEQ_4:21; :: thesis: verum