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