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

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

let j be Nat; :: thesis: ( 1 <= j & j < k implies (f /^ i) . j <> (f /^ i) . k )
assume that
A8: 1 <= j and
A9: j < k ; :: thesis: (f /^ i) . j <> (f /^ i) . k
j <= i + j by NAT_1:11;
then A10: 1 <= i + j by A8, XXREAL_0:2;
i + k = p .. f ;
then A11: i + j < p .. f by A9, XREAL_1:6;
then i + j <= len f by A3, XXREAL_0:2;
then A12: i + j in dom f by A10, FINSEQ_3:25;
j <= len (f /^ i) by A5, A9, XXREAL_0:2;
then j in dom (f /^ i) by A8, FINSEQ_3:25;
then A13: f . (i + j) = (f /^ i) . j by A4, RFINSEQ:def 1;
f . (i + k) = (f /^ i) . k by A4, A6, RFINSEQ:def 1;
hence (f /^ i) . j <> (f /^ i) . k by A1, A13, A11, A12, FINSEQ_4:19, FINSEQ_4:24; :: thesis: verum

end;

(f /^ i) . k = f . (k + i) by A4, A6, RFINSEQ:def 1
.= p by A1, FINSEQ_4:19 ;
then p .. (f /^ i) = k by A6, A7, Th2;
hence i + (p .. (f /^ i)) = p .. f ; :: thesis: verum