for f being FinSequence st 1 <= len f holds
mid (f,1,(len f)) = f