theorem Th67: :: FINSEQ_6:67

for D being non empty set
for p being Element of D
for f1, f2 being FinSequence of D st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) -: p = f1 ^ (f2 -: p)