theorem :: FINSEQ_3:70

for p being FinSequence
for x being object holds
( p - {x} = p iff not x in rng p )