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