let f, g be FinSequence; :: thesis: for x being set st x in rng f holds
x .. f = x .. (f ^' g)
let x be set ; :: thesis: ( x in rng f implies x .. f = x .. (f ^' g) )
assume A1: x in rng f ; :: thesis: x .. f = x .. (f ^' g)
then A2: f . (x .. f) = x by FINSEQ_4:29;
A3: x .. f in dom f by A1, FINSEQ_4:30;
then A4: ( 1 <= x .. f & x .. f <= len f ) by FINSEQ_3:27;
then A5: (f ^' g) . (x .. f) = x by A2, GRAPH_2:14;
len f <= len (f ^' g) by Th7;
then A6: dom f c= dom (f ^' g) by FINSEQ_3:32;
for i being Nat st 1 <= i & i < x .. f holds
(f ^' g) . i <> x

proof

let i be Nat; :: thesis: ( 1 <= i & i < x .. f implies (f ^' g) . i <> x )
assume A7: ( 1 <= i & i < x .. f ) ; :: thesis: (f ^' g) . i <> x
X: i in NAT by ORDINAL1:def 13;
A8: i < len f by A4, A7, XXREAL_0:2;
then A9: (f ^' g) . i = f . i by A7, X, GRAPH_2:14;
i in dom f by A7, A8, FINSEQ_3:27;
hence (f ^' g) . i <> x by A7, A9, FINSEQ_4:34; :: thesis: verum

end;

hence x .. f = x .. (f ^' g) by A3, A5, A6, FINSEQ_6:4; :: thesis: verum