let k be Nat; :: thesis: for D being non empty set
for f being FinSequence of D 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 D be non empty set ; :: thesis: for f being FinSequence of D 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 of D; :: 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
A3: f /. k in rng f by A1, PARTFUN2:2;
assume A4: (f /. k) .. f <> k ; :: thesis: contradiction
(f /. k) .. f <= k by A1, FINSEQ_5:39;
then (f /. k) .. f < k by A4, XXREAL_0:1;
then f /. ((f /. k) .. f) <> f /. k by A2, A3, FINSEQ_4:21;
hence contradiction by A3, FINSEQ_5:38; :: thesis: verum