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

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