for f being XFinSequence holds mid (f,2,(len f)) = f /^ 1