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 A2, XBOOLE_0:def 5;

f -: p1 = (f -| p1) ^ <*p1*> by A1, Th40;

then rng (f -: p1) = (rng (f -| p1)) \/ (rng <*p1*>) by FINSEQ_1:31;

then A4: not p2 in rng <*p1*> by A3, XBOOLE_0:def 3;

rng f = (rng (f -: p1)) \/ (rng (f :- p1)) by A1, Th70;

then A5: p2 in rng (f :- p1) by A2, A3, XBOOLE_0:def 3;

f :- p1 = <*p1*> ^ (f |-- p1) by A1, Th41;

then rng (f :- p1) = (rng <*p1*>) \/ (rng (f |-- p1)) by FINSEQ_1:31;

then p2 in rng (f |-- p1) by A5, A4, XBOOLE_0:def 3;

then A6: p2 in (rng (f |-- p1)) \ (rng <*p1*>) by A4, XBOOLE_0:def 5;

thus (f :- p1) :- p2 = <*p2*> ^ ((f :- p1) |-- p2) by A5, Th41

.= <*p2*> ^ ((<*p1*> ^ (f |-- p1)) |-- p2) by A1, Th41

.= <*p2*> ^ ((f |-- p1) |-- p2) by A6, Th9

.= <*p2*> ^ (f |-- p2) by A1, A2, Th69

.= f :- p2 by A2, Th41 ; :: thesis: verum

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 A2, XBOOLE_0:def 5;

f -: p1 = (f -| p1) ^ <*p1*> by A1, Th40;

then rng (f -: p1) = (rng (f -| p1)) \/ (rng <*p1*>) by FINSEQ_1:31;

then A4: not p2 in rng <*p1*> by A3, XBOOLE_0:def 3;

rng f = (rng (f -: p1)) \/ (rng (f :- p1)) by A1, Th70;

then A5: p2 in rng (f :- p1) by A2, A3, XBOOLE_0:def 3;

f :- p1 = <*p1*> ^ (f |-- p1) by A1, Th41;

then rng (f :- p1) = (rng <*p1*>) \/ (rng (f |-- p1)) by FINSEQ_1:31;

then p2 in rng (f |-- p1) by A5, A4, XBOOLE_0:def 3;

then A6: p2 in (rng (f |-- p1)) \ (rng <*p1*>) by A4, XBOOLE_0:def 5;

thus (f :- p1) :- p2 = <*p2*> ^ ((f :- p1) |-- p2) by A5, Th41

.= <*p2*> ^ ((<*p1*> ^ (f |-- p1)) |-- p2) by A1, Th41

.= <*p2*> ^ ((f |-- p1) |-- p2) by A6, Th9

.= <*p2*> ^ (f |-- p2) by A1, A2, Th69

.= f :- p2 by A2, Th41 ; :: thesis: verum