for F being non empty XFinSequence holds LastLoc F = (card F) -' 1