theorem Th67: :: FINSEQ_3:69

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