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:19;
A3: x .. f in dom f by A1, FINSEQ_4:20;
then A4: x .. f <= len f by FINSEQ_3:25;
A5: 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 that
A6: 1 <= i and
A7: i < x .. f ; :: thesis: (f ^' g) . i <> x
A8: i < len f by A4, A7, XXREAL_0:2;
then A9: i in dom f by A6, FINSEQ_3:25;
(f ^' g) . i = f . i by A6, A8, FINSEQ_6:140;
hence (f ^' g) . i <> x by A7, A9, FINSEQ_4:24; :: thesis: verum

end;

len f <= len (f ^' g) by Th7;
then A10: dom f c= dom (f ^' g) by FINSEQ_3:30;
1 <= x .. f by A3, FINSEQ_3:25;
then (f ^' g) . (x .. f) = x by A2, A4, FINSEQ_6:140;
hence x .. f = x .. (f ^' g) by A3, A10, A5, FINSEQ_6:2; :: thesis: verum