theorem Th66: :: FINSEQ_3:68

for p being FinSequence
for A being set holds
( p - A = {} iff rng p c= A )