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
(f /^ k) -: p = (f -: p) /^ 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
(f /^ k) -: p = (f -: p) /^ k

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & p .. f > k holds
(f /^ k) -: p = (f -: p) /^ k

let f be FinSequence of D; :: thesis: ( p in rng f & p .. f > k implies (f /^ k) -: p = (f -: p) /^ k )
assume that
A1: p in rng f and
A2: p .. f > k ; :: thesis: (f /^ k) -: p = (f -: p) /^ k
A3: p in rng (f /^ k) by A1, A2, Th57;
p .. f = k + (p .. (f /^ k)) by A1, A2, Th56;
then A4: len ((f /^ k) -: p) = (p .. f) - k by
.= (len (f -: p)) - k by ;
A5: now :: thesis: for m being Nat st m in dom ((f /^ k) -: p) holds
((f /^ k) -: p) . m = (f -: p) . (m + k)
let m be Nat; :: thesis: ( m in dom ((f /^ k) -: p) implies ((f /^ k) -: p) . m = (f -: p) . (m + k) )
A6: m + k >= m by NAT_1:11;
reconsider M = m as Nat ;
assume A7: m in dom ((f /^ k) -: p) ; :: thesis: ((f /^ k) -: p) . m = (f -: p) . (m + k)
then m <= (len (f -: p)) - k by ;
then A8: m + k <= len (f -: p) by XREAL_1:19;
1 <= m by ;
then 1 <= m + k by ;
then A9: M + k in dom (f -: p) by ;
len ((f /^ k) -: p) = p .. (f /^ k) by ;
then A10: m in Seg (p .. (f /^ k)) by ;
(f /^ k) -: p = (f /^ k) | (p .. (f /^ k)) by FINSEQ_5:def 1;
then A11: dom ((f /^ k) -: p) c= dom (f /^ k) by FINSEQ_5:18;
len (f -: p) = p .. f by ;
then A12: m + k in Seg (p .. f) by ;
thus ((f /^ k) -: p) . m = ((f /^ k) -: p) /. m by
.= (f /^ k) /. m by
.= f /. (m + k) by
.= (f -: p) /. (M + k) by
.= (f -: p) . (m + k) by ; :: thesis: verum
end;
k <= len (f -: p) by ;
hence (f /^ k) -: p = (f -: p) /^ k by ; :: thesis: verum