for X being non empty set
for f, g being FinSequence of X st g is_Shortcut_of f holds
( 1 <= len g & len g <= len f )