theorem Th94: :: FINSEQ_3:96

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