theorem :: VALUED_1:65

for F being NAT -defined non empty finite Function holds card (CutLastLoc F) = (card F) -' 1