let f1, f2 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
then A2: (len f1) + (p .. f2) = p .. (f1 ^ f2) by Th7;
A3: now :: thesis: for k being Nat st k in dom (f2 |-- p) holds
(f2 |-- p) . k = (f1 ^ f2) . (k + (p .. (f1 ^ f2)))
let k be Nat; :: thesis: ( k in dom (f2 |-- p) implies (f2 |-- p) . k = (f1 ^ f2) . (k + (p .. (f1 ^ f2))) )
A4: k <= k + (p .. f2) by NAT_1:11;
len (f2 |-- p) = (len f2) - (p .. f2) by ;
then A5: (len (f2 |-- p)) + (p .. f2) = len f2 ;
assume A6: k in dom (f2 |-- p) ; :: thesis: (f2 |-- p) . k = (f1 ^ f2) . (k + (p .. (f1 ^ f2)))
then k <= len (f2 |-- p) by FINSEQ_3:25;
then A7: k + (p .. f2) <= len f2 by ;
1 <= k by ;
then 1 <= k + (p .. f2) by ;
then A8: k + (p .. f2) in dom f2 by ;
thus (f2 |-- p) . k = f2 . (k + (p .. f2)) by
.= (f1 ^ f2) . ((len f1) + (k + (p .. f2))) by
.= (f1 ^ f2) . (k + (p .. (f1 ^ f2))) by A2 ; :: thesis: verum
end;
rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31;
then A9: p in rng (f1 ^ f2) by ;
len (f2 |-- p) = (len f2) - (p .. f2) by
.= ((len f1) + (len f2)) - ((len f1) + (p .. f2))
.= (len (f1 ^ f2)) - (p .. (f1 ^ f2)) by ;
hence (f1 ^ f2) |-- p = f2 |-- p by ; :: thesis: verum