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 ; :: 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 ;
then rng (f -: p1) = (rng (f -| p1)) \/ (rng <*p1*>) by FINSEQ_1:31;
then A4: p2 in rng (f -| p1) by ;
A5: rng (f -| p1) c= rng f by ;
thus (f -: p1) -: p2 = ((f -: p1) -| p2) ^ <*p2*> by
.= (((f -| p1) ^ <*p1*>) -| p2) ^ <*p2*> by
.= ((f -| p1) -| p2) ^ <*p2*> by
.= (f -| p2) ^ <*p2*> by A1, A4, Th35
.= f -: p2 by A4, A5, Th40 ; :: thesis: verum
end;
end;