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 ;
A3: p .. f <= len f by ;
then A4: i <= len f by ;
(p .. f) - i <= (len f) - i by ;
then A5: k <= len (f /^ i) by ;
k <> 0 by A2;
then 1 <= k by NAT_1:14;
then A6: k in dom (f /^ i) by ;
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 ;
i + k = p .. f ;
then A11: i + j < p .. f by ;
then i + j <= len f by ;
then A12: i + j in dom f by ;
j <= len (f /^ i) by ;
then j in dom (f /^ i) by ;
then A13: f . (i + j) = (f /^ i) . j by ;
f . (i + k) = (f /^ i) . k by ;
hence (f /^ i) . j <> (f /^ i) . k by ; :: thesis: verum
end;
(f /^ i) . k = f . (k + i) by
.= p by ;
then p .. (f /^ i) = k by A6, A7, Th2;
hence i + (p .. (f /^ i)) = p .. f ; :: thesis: verum