theorem Th96: :: FINSEQ_3:98

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