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 )
A1: dom f1 c= dom (f1 ^ f2) by FINSEQ_1:26;
assume A2: p in rng f1 ; :: thesis: p .. (f1 ^ f2) = p .. f1
then A3: p .. f1 in dom f1 by FINSEQ_4:20;
A4: now :: thesis: for i being Nat st 1 <= i & i < p .. f1 holds
(f1 ^ f2) . i <> (f1 ^ f2) . (p .. f1)
A5: (f1 ^ f2) . (p .. f1) = f1 . (p .. f1) by A3, FINSEQ_1:def 7;
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 A2, FINSEQ_4:21;
then i <= len f1 by A7, XXREAL_0:2;
then A8: i in dom f1 by A6, FINSEQ_3:25;
then (f1 ^ f2) . i = f1 . i by FINSEQ_1:def 7;
hence (f1 ^ f2) . i <> (f1 ^ f2) . (p .. f1) by A2, A7, A8, A5, FINSEQ_4:19, FINSEQ_4:24; :: thesis: verum
end;
f1 . (p .. f1) = p by A2, FINSEQ_4:19;
then (f1 ^ f2) . (p .. f1) = p by A3, FINSEQ_1:def 7;
hence p .. (f1 ^ f2) = p .. f1 by A3, A1, A4, Th2; :: thesis: verum