theorem :: FINSEQ_3:87

for p being FinSequence
for A being set st p is one-to-one holds
p - A is one-to-one ;