theorem Th98: :: FINSEQ_3:100

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