theorem :: FINSEQ_3:67

for p being FinSequence
for A being set st rng (p - A) = rng p holds
A misses rng p