let f1, f2 be FinSequence; :: thesis: for p being set st p in rng f1 holds
p .. (f1 ^ f2) = p .. f1
let p be set ; :: thesis: ( p in rng f1 implies p .. (f1 ^ f2) = p .. f1 )
assume A1: p in rng f1 ; :: thesis: p .. (f1 ^ f2) = p .. f1
then A2: f1 . (p .. f1) = p by FINSEQ_4:29;
A3: p .. f1 in dom f1 by A1, FINSEQ_4:30;
then A4: (f1 ^ f2) . (p .. f1) = p by A2, FINSEQ_1:def 7;
A5: dom f1 c= dom (f1 ^ f2) by FINSEQ_1:39;

now

let i be Nat; :: thesis: ( 1 <= i & i < p .. f1 implies (f1 ^ f2) . i <> (f1 ^ f2) . (p .. f1) )
assume that
A6: 1 <= i and
A7: i < p .. f1 ; :: thesis: (f1 ^ f2) . i <> (f1 ^ f2) . (p .. f1)
p .. f1 <= len f1 by A1, FINSEQ_4:31;
then i <= len f1 by A7, XXREAL_0:2;
then A8: i in dom f1 by A6, FINSEQ_3:27;
A9: (f1 ^ f2) . (p .. f1) = f1 . (p .. f1) by A3, FINSEQ_1:def 7;
(f1 ^ f2) . i = f1 . i by A8, FINSEQ_1:def 7;
hence (f1 ^ f2) . i <> (f1 ^ f2) . (p .. f1) by A1, A7, A8, A9, FINSEQ_4:29, FINSEQ_4:34; :: thesis: verum

end;

hence p .. (f1 ^ f2) = p .. f1 by A3, A4, A5, Th4; :: thesis: verum