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

now

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

end;

then p .. (f /^ i) = k by A7, A8, Th4;
hence i + (p .. (f /^ i)) = p .. f ; :: thesis: verum