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: p .. f <= len (f -: p) by FINSEQ_5:42;
A3: now :: thesis: for i being Nat st 1 <= i & i < p .. f holds
(f -: p) /. i <> (f -: p) /. (p .. f)
p .. f <> 0 by A1, FINSEQ_4:21;
then p .. f in Seg (p .. f) by FINSEQ_1:3;
then A4: (f -: p) /. (p .. f) = f /. (p .. f) by A1, FINSEQ_5:43;
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;
then A7: (f -: p) /. i = f /. i by A1, FINSEQ_5:43;
p .. f <= len f by A1, FINSEQ_4:21;
then i <= len f by A6, XXREAL_0:2;
then A8: i in dom f by A5, FINSEQ_3:25;
f /. (p .. f) = p by A1, FINSEQ_5:38;
hence (f -: p) /. i <> (f -: p) /. (p .. f) by A6, A7, A4, A8, FINSEQ_5:39; :: thesis: verum
end;
1 <= p .. f by A1, FINSEQ_4:21;
then A9: p .. f in dom (f -: p) by A2, FINSEQ_3:25;
(f -: p) /. (p .. f) = p by A1, FINSEQ_5:45;
hence p .. (f -: p) = p .. f by A9, A3, Th48; :: thesis: verum