let D be non empty set ; :: thesis: for p1, p2 being Element of D
for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds
(f :- p1) :- p2 = f :- p2

let p1, p2 be Element of D; :: thesis: for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds
(f :- p1) :- p2 = f :- p2

let f be FinSequence of D; :: thesis: ( p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) implies (f :- p1) :- p2 = f :- p2 )
assume that
A1: p1 in rng f and
A2: p2 in (rng f) \ (rng (f -: p1)) ; :: thesis: (f :- p1) :- p2 = f :- p2
A3: not p2 in rng (f -: p1) by ;
f -: p1 = (f -| p1) ^ <*p1*> by ;
then rng (f -: p1) = (rng (f -| p1)) \/ (rng <*p1*>) by FINSEQ_1:31;
then A4: not p2 in rng <*p1*> by ;
rng f = (rng (f -: p1)) \/ (rng (f :- p1)) by ;
then A5: p2 in rng (f :- p1) by ;
f :- p1 = <*p1*> ^ (f |-- p1) by ;
then rng (f :- p1) = (rng <*p1*>) \/ (rng (f |-- p1)) by FINSEQ_1:31;
then p2 in rng (f |-- p1) by ;
then A6: p2 in (rng (f |-- p1)) \ (rng <*p1*>) by ;
thus (f :- p1) :- p2 = <*p2*> ^ ((f :- p1) |-- p2) by
.= <*p2*> ^ ((<*p1*> ^ (f |-- p1)) |-- p2) by
.= <*p2*> ^ ((f |-- p1) |-- p2) by
.= <*p2*> ^ (f |-- p2) by A1, A2, Th69
.= f :- p2 by ; :: thesis: verum