let f1, f2 be FinSequence; :: thesis: for p being set st p in rng f1 holds
(f1 ^ f2) -| p = f1 -| p
let p be set ; :: thesis: ( p in rng f1 implies (f1 ^ f2) -| p = f1 -| p )
assume A1: p in rng f1 ; :: thesis: (f1 ^ f2) -| p = f1 -| p
then consider n being Nat such that
A2: n = (p .. f1) - 1 and
A3: f1 | (Seg n) = f1 -| p by FINSEQ_4:def 5;
A4: p .. f1 <= len f1 by A1, FINSEQ_4:21;
n + 1 = p .. f1 by A2;
then n <= p .. f1 by NAT_1:11;
then n <= len f1 by A4, XXREAL_0:2;
then Seg n c= Seg (len f1) by FINSEQ_1:5;
then Seg n c= dom f1 by FINSEQ_1:def 3;
then A5: (f1 ^ f2) | (Seg n) = f1 | (Seg n) by Th10, GRFUNC_1:27;
rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31;
then A6: p in rng (f1 ^ f2) by A1, XBOOLE_0:def 3;
n = (p .. (f1 ^ f2)) - 1 by A1, A2, Th6;
hence (f1 ^ f2) -| p = f1 -| p by A3, A6, A5, FINSEQ_4:def 5; :: thesis: verum