let f1, f2 be FinSequence; :: thesis: for p being set st p in rng f1 holds
(f1 ^ f2) |-- p = (f1 |-- p) ^ f2
let p be set ; :: thesis: ( p in rng f1 implies (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 )
assume A1: p in rng f1 ; :: thesis: (f1 ^ f2) |-- p = (f1 |-- p) ^ f2
rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:44;
then A2: p in rng (f1 ^ f2) by A1, XBOOLE_0:def 3;
A3: p .. f1 = p .. (f1 ^ f2) by A1, Th8;
A4: len (f1 |-- p) = (len f1) - (p .. f1) by A1, FINSEQ_4:def 7;
then A5: len ((f1 |-- p) ^ f2) = ((len f1) - (p .. f1)) + (len f2) by FINSEQ_1:35
.= ((len f1) + (len f2)) - (p .. f1)
.= (len (f1 ^ f2)) - (p .. (f1 ^ f2)) by A3, FINSEQ_1:35 ;

now

let k be Nat; :: thesis: ( k in dom ((f1 |-- p) ^ f2) implies ((f1 |-- p) ^ f2) . b₁ = (f1 ^ f2) . (b₁ + (p .. (f1 ^ f2))) )
assume A6: k in dom ((f1 |-- p) ^ f2) ; :: thesis: ((f1 |-- p) ^ f2) . b₁ = (f1 ^ f2) . (b₁ + (p .. (f1 ^ f2)))

per cases ( k in dom (f1 |-- p) or ex n being Nat st
( n in dom f2 & k = (len (f1 |-- p)) + n ) ) by A6, FINSEQ_1:38;

suppose A7: k in dom (f1 |-- p) ; :: thesis: ((f1 |-- p) ^ f2) . b₁ = (f1 ^ f2) . (b₁ + (p .. (f1 ^ f2)))

then ( 1 <= k & k <= k + (p .. f1) ) by FINSEQ_3:27, NAT_1:11;
then A8: 1 <= k + (p .. f1) by XXREAL_0:2;
A9: k <= len (f1 |-- p) by A7, FINSEQ_3:27;
len (f1 |-- p) = (len f1) - (p .. f1) by A1, FINSEQ_4:def 7;
then (len (f1 |-- p)) + (p .. f1) = len f1 ;
then k + (p .. f1) <= len f1 by A9, XREAL_1:8;
then A10: k + (p .. f1) in dom f1 by A8, FINSEQ_3:27;
thus ((f1 |-- p) ^ f2) . k = (f1 |-- p) . k by A7, FINSEQ_1:def 7
.= f1 . (k + (p .. f1)) by A1, A7, FINSEQ_4:def 7
.= (f1 ^ f2) . (k + (p .. (f1 ^ f2))) by A3, A10, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom f2 & k = (len (f1 |-- p)) + n ) ; :: thesis: ((f1 |-- p) ^ f2) . b₁ = (f1 ^ f2) . (b₁ + (p .. (f1 ^ f2)))

then consider n being Nat such that
A11: n in dom f2 and
A12: k = (len (f1 |-- p)) + n ;
thus ((f1 |-- p) ^ f2) . k = f2 . n by A11, A12, FINSEQ_1:def 7
.= (f1 ^ f2) . ((len f1) + n) by A11, FINSEQ_1:def 7
.= (f1 ^ f2) . (k + (p .. (f1 ^ f2))) by A3, A4, A12 ; :: thesis: verum

end;

end;

end;

hence (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 by A2, A5, FINSEQ_4:def 7; :: thesis: verum