theorem Th86: :: FINSEQ_3:88

for p being FinSequence
for A being set st p is one-to-one holds
len (p - A) = (len p) - (card (A /\ (rng p)))