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

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 )
;

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;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