theorem :: FINSEQ_3:97

for p being FinSequence
for x being object st p is one-to-one & rng p = {x} holds
p = <*x*>