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 ;
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 ;
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 ;
then A7: (len (f1 |-- p)) + (p .. f1) = len f1 ;
k <= len (f1 |-- p) by ;
then A8: k + (p .. f1) <= len f1 by ;
A9: k <= k + (p .. f1) by NAT_1:11;
1 <= k by ;
then 1 <= k + (p .. f1) by ;
then A10: k + (p .. f1) in dom f1 by ;
thus ((f1 |-- p) ^ f2) . k = (f1 |-- p) . k by
.= f1 . (k + (p .. f1)) by
.= (f1 ^ f2) . (k + (p .. (f1 ^ f2))) by ; :: 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
.= (f1 ^ f2) . ((len f1) + n) by
.= (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 ;
len ((f1 |-- p) ^ f2) = ((len f1) - (p .. f1)) + (len f2) by
.= ((len f1) + (len f2)) - (p .. f1)
.= (len (f1 ^ f2)) - (p .. (f1 ^ f2)) by ;
hence (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 by ; :: thesis: verum