theorem :: FINSEQ_3:101

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