let k be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f > k holds
p .. f = k + (p .. (f /^ k))
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f & p .. f > k holds
p .. f = k + (p .. (f /^ k))
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & p .. f > k holds
p .. f = k + (p .. (f /^ k))
let f be FinSequence of D; :: thesis: ( p in rng f & p .. f > k implies p .. f = k + (p .. (f /^ k)) )
assume that
A1: p in rng f and
A2: p .. f > k ; :: thesis: p .. f = k + (p .. (f /^ k))
reconsider i = (p .. f) - k as Element of NAT by A2, INT_1:5;
A3: i + k <= len f by A1, FINSEQ_4:21;
then A4: i <= (len f) - k by XREAL_1:19;
k <= k + i by NAT_1:11;
then k <= len f by A3, XXREAL_0:2;
then A5: i <= len (f /^ k) by A4, RFINSEQ:def 1;
i <> 0 by A2;
then 1 <= i by NAT_1:14;
then A6: i in dom (f /^ k) by A5, FINSEQ_3:25;
A7: k + i = p .. f ;

A8: now :: thesis: for j being Nat st 1 <= j & j < i holds
(f /^ k) /. j <> (f /^ k) /. i

let j be Nat; :: thesis: ( 1 <= j & j < i implies (f /^ k) /. j <> (f /^ k) /. i )
assume that
A9: 1 <= j and
A10: j < i ; :: thesis: (f /^ k) /. j <> (f /^ k) /. i
reconsider J = j as Nat ;
k + j >= j by NAT_1:11;
then A11: 1 <= k + j by A9, XXREAL_0:2;
j <= len (f /^ k) by A5, A10, XXREAL_0:2;
then j in dom (f /^ k) by A9, FINSEQ_3:25;
then A12: f /. (k + j) = (f /^ k) /. j by FINSEQ_5:27;
A13: k + i <= len f by A1, FINSEQ_4:21;
k + j < k + i by A10, XREAL_1:6;
then k + j <= len f by A13, XXREAL_0:2;
then A14: k + J in dom f by A11, FINSEQ_3:25;
k + j < p .. f by A7, A10, XREAL_1:6;
then A15: f /. (k + j) <> p by A14, FINSEQ_5:39;
f /. (k + i) = (f /^ k) /. i by A6, FINSEQ_5:27;
hence (f /^ k) /. j <> (f /^ k) /. i by A1, A12, A15, FINSEQ_5:38; :: thesis: verum

end;

(f /^ k) /. i = f /. (k + i) by A6, FINSEQ_5:27
.= p by A1, FINSEQ_5:38 ;
then (p .. f) - k = p .. (f /^ k) by A6, A8, Th48;
hence p .. f = k + (p .. (f /^ k)) ; :: thesis: verum