let F be NAT -defined non empty finite Function; :: thesis: card (CutLastLoc F) = (card F) -' 1
A1: card F >= 0 + 1 by NAT_1:13;
thus card (CutLastLoc F) = (card F) - 1 by Th37
.= (card F) -' 1 by A1, XREAL_1:233 ; :: thesis: verum