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

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