theorem Th64: :: FINSEQ_6:64

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