theorem :: FINSEQ_3:90

for p being FinSequence
for x being object st p is one-to-one & x in rng p holds
len (p - {x}) = (len p) - 1