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, Th79; :: 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:56;
f -: p1 = (f -| p1) ^ <*p1*> by A1, Th44;
then rng (f -: p1) = (rng (f -| p1)) \/ (rng <*p1*>) by FINSEQ_1:44;
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:51;
thus (f -: p1) -: p2 = ((f -: p1) -| p2) ^ <*p2*> by A2, Th44
.= (((f -| p1) ^ <*p1*>) -| p2) ^ <*p2*> by A1, Th44
.= ((f -| p1) -| p2) ^ <*p2*> by A4, Th14
.= (f -| p2) ^ <*p2*> by A1, A4, Th39
.= f -: p2 by A4, A5, Th44 ; :: thesis: verum

end;

end;