theorem Th15: :: FINSEQ_6:15

for f1, f2 being FinSequence
for p being set st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) -| p = f1 ^ (f2 -| p)