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