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 |-- p2 = (f |-- p1) |-- 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 |-- p2 = (f |-- p1) |-- p2
let f be FinSequence of D; :: thesis: ( p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) implies f |-- p2 = (f |-- p1) |-- p2 )
assume that
A1: p1 in rng f and
A2: p2 in (rng f) \ (rng (f -: p1)) ; :: thesis: f |-- p2 = (f |-- p1) |-- p2
not p2 in rng (f -: p1) by A2, XBOOLE_0:def 5;
then A3: not p2 in rng ((f -| p1) ^ <*p1*>) by A1, Th40;
f = ((f -| p1) ^ <*p1*>) ^ (f |-- p1) by A1, FINSEQ_4:51;
then rng f = (rng ((f -| p1) ^ <*p1*>)) \/ (rng (f |-- p1)) by FINSEQ_1:31;
then p2 in rng (f |-- p1) by A2, A3, XBOOLE_0:def 3;
then A4: p2 in (rng (f |-- p1)) \ (rng ((f -| p1) ^ <*p1*>)) by A3, XBOOLE_0:def 5;
thus f |-- p2 = (((f -| p1) ^ <*p1*>) ^ (f |-- p1)) |-- p2 by A1, FINSEQ_4:51
.= (f |-- p1) |-- p2 by A4, Th9 ; :: thesis: verum