let f2, f1 be FinSequence; :: thesis: for p being set st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) |-- p = f2 |-- p
let p be set ; :: thesis: ( p in (rng f2) \ (rng f1) implies (f1 ^ f2) |-- p = f2 |-- p )
assume A1: p in (rng f2) \ (rng f1) ; :: thesis: (f1 ^ f2) |-- p = f2 |-- p
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: (len f1) + (p .. f2) = p .. (f1 ^ f2) by A1, Th9;
A4: len (f2 |-- p) = (len f2) - (p .. f2) by A1, FINSEQ_4:def 7
.= ((len f1) + (len f2)) - ((len f1) + (p .. f2))
.= (len (f1 ^ f2)) - (p .. (f1 ^ f2)) by A3, FINSEQ_1:35 ;

now

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

end;

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