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: k <= len (f -: p) by A1, A2, FINSEQ_5:45;
A4: p .. f = k + (p .. (f /^ k)) by A1, A2, Th61;
A5: p in rng (f /^ k) by A1, A2, Th62;
then A6: len ((f /^ k) -: p) = (p .. f) - k by A4, FINSEQ_5:45
.= (len (f -: p)) - k by A1, FINSEQ_5:45 ;

now

let m be Nat; :: thesis: ( m in dom ((f /^ k) -: p) implies ((f /^ k) -: p) . m = (f -: p) . (m + k) )
assume A7: m in dom ((f /^ k) -: p) ; :: thesis: ((f /^ k) -: p) . m = (f -: p) . (m + k)
A8: m + k >= m by NAT_1:11;
reconsider M = m as Element of NAT by ORDINAL1:def 13;
( 1 <= m & m <= (len (f -: p)) - k ) by A6, A7, FINSEQ_3:27;
then ( 1 <= m + k & m + k <= len (f -: p) ) by A8, XREAL_1:21, XXREAL_0:2;
then A9: M + k in dom (f -: p) by FINSEQ_3:27;
len (f -: p) = p .. f by A1, FINSEQ_5:45;
then A10: m + k in Seg (p .. f) by A9, FINSEQ_1:def 3;
len ((f /^ k) -: p) = p .. (f /^ k) by A5, FINSEQ_5:45;
then A11: m in Seg (p .. (f /^ k)) by A7, FINSEQ_1:def 3;
(f /^ k) -: p = (f /^ k) | (p .. (f /^ k)) by FINSEQ_5:def 1;
then A12: dom ((f /^ k) -: p) c= dom (f /^ k) by FINSEQ_5:20;
thus ((f /^ k) -: p) . m = ((f /^ k) -: p) /. m by A7, PARTFUN1:def 8
.= (f /^ k) /. m by A5, A11, FINSEQ_5:46
.= f /. (m + k) by A7, A12, FINSEQ_5:30
.= (f -: p) /. (M + k) by A1, A10, FINSEQ_5:46
.= (f -: p) . (m + k) by A9, PARTFUN1:def 8 ; :: thesis: verum

end;

hence (f /^ k) -: p = (f -: p) /^ k by A3, A6, RFINSEQ:def 2; :: thesis: verum