theorem :: FINSEQ_3:99

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