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 ;
A3: i + k <= len f by ;
then A4: i <= (len f) - k by XREAL_1:19;
k <= k + i by NAT_1:11;
then k <= len f by ;
then A5: i <= len (f /^ k) by ;
i <> 0 by A2;
then 1 <= i by NAT_1:14;
then A6: i in dom (f /^ k) by ;
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 ;
j <= len (f /^ k) by ;
then j in dom (f /^ k) by ;
then A12: f /. (k + j) = (f /^ k) /. j by FINSEQ_5:27;
A13: k + i <= len f by ;
k + j < k + i by ;
then k + j <= len f by ;
then A14: k + J in dom f by ;
k + j < p .. f by ;
then A15: f /. (k + j) <> p by ;
f /. (k + i) = (f /^ k) /. i by ;
hence (f /^ k) /. j <> (f /^ k) /. i by ; :: thesis: verum
end;
(f /^ k) /. i = f /. (k + i) by
.= p by ;
then (p .. f) - k = p .. (f /^ k) by A6, A8, Th48;
hence p .. f = k + (p .. (f /^ k)) ; :: thesis: verum