theorem Th35: :: FINSEQ_6:35

for x, y being set
for f being FinSequence st x in rng f & y in rng (f -| x) holds
(f -| x) -| y = f -| y