theorem :: FINSEQ_3:62

for p being FinSequence
for A being set
for n being Nat st n = (len p) - (card (p " A)) holds
dom (p - A) = Seg n