let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f holds
p .. (f -: p) = p .. f
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
p .. (f -: p) = p .. f
let f be FinSequence of D; :: thesis: ( p in rng f implies p .. (f -: p) = p .. f )
assume A1: p in rng f ; :: thesis: p .. (f -: p) = p .. f
then A2: (f -: p) /. (p .. f) = p by FINSEQ_5:48;
A3: 1 <= p .. f by A1, FINSEQ_4:31;
p .. f <= len (f -: p) by A1, FINSEQ_5:45;
then A4: p .. f in dom (f -: p) by A3, FINSEQ_3:27;

now

let i be Nat; :: thesis: ( 1 <= i & i < p .. f implies (f -: p) /. i <> (f -: p) /. (p .. f) )
assume that
A5: 1 <= i and
A6: i < p .. f ; :: thesis: (f -: p) /. i <> (f -: p) /. (p .. f)
i in Seg (p .. f) by A5, A6, FINSEQ_1:3;
then A7: (f -: p) /. i = f /. i by A1, FINSEQ_5:46;
p .. f <> 0 by A1, FINSEQ_4:31;
then p .. f in Seg (p .. f) by FINSEQ_1:5;
then A8: (f -: p) /. (p .. f) = f /. (p .. f) by A1, FINSEQ_5:46;
A9: f /. (p .. f) = p by A1, FINSEQ_5:41;
p .. f <= len f by A1, FINSEQ_4:31;
then i <= len f by A6, XXREAL_0:2;
then i in dom f by A5, FINSEQ_3:27;
hence (f -: p) /. i <> (f -: p) /. (p .. f) by A6, A7, A8, A9, FINSEQ_5:42; :: thesis: verum

end;

hence p .. (f -: p) = p .. f by A2, A4, Th52; :: thesis: verum