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
then A2: p .. f1 = p .. (f1 ^ f2) by Th6;
A3: len (f1 |-- p) = (len f1) - (p .. f1) by A1, FINSEQ_4:def 6;
A4: now :: thesis: for k being Nat st k in dom ((f1 |-- p) ^ f2) holds
((f1 |-- p) ^ f2) . k = (f1 ^ f2) . (k + (p .. (f1 ^ f2)))
let k be Nat; :: thesis: ( k in dom ((f1 |-- p) ^ f2) implies ((f1 |-- p) ^ f2) . b1 = (f1 ^ f2) . (b1 + (p .. (f1 ^ f2))) )
assume A5: k in dom ((f1 |-- p) ^ f2) ; :: thesis: ((f1 |-- p) ^ f2) . b1 = (f1 ^ f2) . (b1 + (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 A5, FINSEQ_1:25;
suppose A6: k in dom (f1 |-- p) ; :: thesis: ((f1 |-- p) ^ f2) . b1 = (f1 ^ f2) . (b1 + (p .. (f1 ^ f2)))
len (f1 |-- p) = (len f1) - (p .. f1) by A1, FINSEQ_4:def 6;
then A7: (len (f1 |-- p)) + (p .. f1) = len f1 ;
k <= len (f1 |-- p) by A6, FINSEQ_3:25;
then A8: k + (p .. f1) <= len f1 by A7, XREAL_1:6;
A9: k <= k + (p .. f1) by NAT_1:11;
1 <= k by A6, FINSEQ_3:25;
then 1 <= k + (p .. f1) by A9, XXREAL_0:2;
then A10: k + (p .. f1) in dom f1 by A8, FINSEQ_3:25;
thus ((f1 |-- p) ^ f2) . k = (f1 |-- p) . k by A6, FINSEQ_1:def 7
.= f1 . (k + (p .. f1)) by A1, A6, FINSEQ_4:def 6
.= (f1 ^ f2) . (k + (p .. (f1 ^ f2))) by A2, 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) . b1 = (f1 ^ f2) . (b1 + (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 A2, A3, A12 ; :: thesis: verum
end;
end;
end;
rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31;
then A13: p in rng (f1 ^ f2) by A1, XBOOLE_0:def 3;
len ((f1 |-- p) ^ f2) = ((len f1) - (p .. f1)) + (len f2) by A3, FINSEQ_1:22
.= ((len f1) + (len f2)) - (p .. f1)
.= (len (f1 ^ f2)) - (p .. (f1 ^ f2)) by A2, FINSEQ_1:22 ;
hence (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 by A13, A4, FINSEQ_4:def 6; :: thesis: verum