theorem :: AFINSQ_1:91

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