for X being non empty set
for f being FinSequence of X st f is one-to-one & len f > 1 holds
( PairF f is Simple & f . 1 <> f . (len f) )