theorem Th8: :: TOPREAL8:8
for f, g being FinSequence
for x being set st x in rng f holds
x .. f = x .. (f ^' g)