let I be non empty XFinSequence; :: thesis: LastLoc I = (card I) - 1
A1: card I >= 0 + 1 by NAT_1:13;
thus LastLoc I = (card I) -' 1 by Th67
.= (card I) - 1 by A1, XREAL_1:233 ; :: thesis: verum