theorem Th12: :: FINSEQ_6:12

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