let f1, f2 be FinSequence; :: thesis: for p being set st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) -| p = f1 ^ (f2 -| p)
let p be set ; :: thesis: ( p in (rng f2) \ (rng f1) implies (f1 ^ f2) -| p = f1 ^ (f2 -| p) )
assume A1: p in (rng f2) \ (rng f1) ; :: thesis: (f1 ^ f2) -| p = f1 ^ (f2 -| p)
then consider n being Nat such that
A2: n = (p .. f2) - 1 and
A3: f2 | (Seg n) = f2 -| p by FINSEQ_4:def 5;
p .. (f1 ^ f2) = (len f1) + (p .. f2) by A1, Th7;
then A4: (len f1) + n = (p .. (f1 ^ f2)) - 1 by A2;
rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31;
then A5: p in rng (f1 ^ f2) by A1, XBOOLE_0:def 3;
(f1 ^ f2) | (Seg ((len f1) + n)) = f1 ^ (f2 -| p) by A3, Th14;
hence (f1 ^ f2) -| p = f1 ^ (f2 -| p) by A5, A4, FINSEQ_4:def 5; :: thesis: verum