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 -: 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 -: p1) holds
(f -: p1) -: p2 = f -: p2
let f be FinSequence of D; :: thesis: ( p1 in rng f & p2 in rng (f -: p1) implies (f -: p1) -: p2 = f -: p2 )
assume that
A1: p1 in rng f and
A2: p2 in rng (f -: p1) ; :: thesis: (f -: p1) -: p2 = f -: p2

per cases ( p1 = p2 or p1 <> p2 ) ;

suppose p1 = p2 ; :: thesis: (f -: p1) -: p2 = f -: p2

hence (f -: p1) -: p2 = f -: p2 by A1, Th74; :: thesis: verum

end;

suppose p1 <> p2 ; :: thesis: (f -: p1) -: p2 = f -: p2

then not p2 in {p1} by TARSKI:def 1;
then A3: not p2 in rng <*p1*> by FINSEQ_1:39;
f -: p1 = (f -| p1) ^ <*p1*> by A1, Th40;
then rng (f -: p1) = (rng (f -| p1)) \/ (rng <*p1*>) by FINSEQ_1:31;
then A4: p2 in rng (f -| p1) by A2, A3, XBOOLE_0:def 3;
A5: rng (f -| p1) c= rng f by A1, FINSEQ_4:39;
thus (f -: p1) -: p2 = ((f -: p1) -| p2) ^ <*p2*> by A2, Th40
.= (((f -| p1) ^ <*p1*>) -| p2) ^ <*p2*> by A1, Th40
.= ((f -| p1) -| p2) ^ <*p2*> by A4, Th12
.= (f -| p2) ^ <*p2*> by A1, A4, Th35
.= f -: p2 by A4, A5, Th40 ; :: thesis: verum

end;

end;