for f being FinSequence st 2 <= len f holds
(f /^ 1) . (len (f /^ 1)) = f . (len f)