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:18;
A3: k + i = p .. f ;
i <> 0 by A2;
then A4: 1 <= i by NAT_1:14;
A5: i + k <= len f by A1, FINSEQ_4:31;
then A6: i <= (len f) - k by XREAL_1:21;
k <= k + i by NAT_1:11;
then k <= len f by A5, XXREAL_0:2;
then A7: i <= len (f /^ k) by A6, RFINSEQ:def 2;
then A8: i in dom (f /^ k) by A4, FINSEQ_3:27;
then A9: (f /^ k) /. i = f /. (k + i) by FINSEQ_5:30
.= p by A1, FINSEQ_5:41 ;

now

let j be Nat; :: thesis: ( 1 <= j & j < i implies (f /^ k) /. j <> (f /^ k) /. i )
assume that
A10: 1 <= j and
A11: j < i ; :: thesis: (f /^ k) /. j <> (f /^ k) /. i
reconsider J = j as Element of NAT by ORDINAL1:def 13;
j <= len (f /^ k) by A7, A11, XXREAL_0:2;
then j in dom (f /^ k) by A10, FINSEQ_3:27;
then A12: f /. (k + j) = (f /^ k) /. j by FINSEQ_5:30;
A13: f /. (k + i) = (f /^ k) /. i by A8, FINSEQ_5:30;
A14: k + j < k + i by A11, XREAL_1:8;
( k + j >= j & k + i <= len f ) by A1, FINSEQ_4:31, NAT_1:11;
then ( 1 <= k + j & k + j <= len f ) by A10, A14, XXREAL_0:2;
then A15: k + J in dom f by FINSEQ_3:27;
k + j < p .. f by A3, A11, XREAL_1:8;
then f /. (k + j) <> p by A15, FINSEQ_5:42;
hence (f /^ k) /. j <> (f /^ k) /. i by A1, A12, A13, FINSEQ_5:41; :: thesis: verum

end;

then (p .. f) - k = p .. (f /^ k) by A8, A9, Th52;
hence p .. f = k + (p .. (f /^ k)) ; :: thesis: verum