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 A1, FINSEQ_4:def 6;
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 A5, XREAL_1:6;
1 <= k by A6, FINSEQ_3:25;
then 1 <= k + (p .. f2) by A4, XXREAL_0:2;
then A8: k + (p .. f2) in dom f2 by A7, FINSEQ_3:25;
thus (f2 |-- p) . k = f2 . (k + (p .. f2)) by A1, A6, FINSEQ_4:def 6
.= (f1 ^ f2) . ((len f1) + (k + (p .. f2))) by A8, FINSEQ_1:def 7
.= (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 A1, XBOOLE_0:def 3;
len (f2 |-- p) = (len f2) - (p .. f2) by A1, FINSEQ_4:def 6
.= ((len f1) + (len f2)) - ((len f1) + (p .. f2))
.= (len (f1 ^ f2)) - (p .. (f1 ^ f2)) by A2, FINSEQ_1:22 ;
hence (f1 ^ f2) |-- p = f2 |-- p by A9, A3, FINSEQ_4:def 6; :: thesis: verum