let D be non empty set ; 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; 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; ( 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))
; (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
; verum