theorem Th37: :: VALUED_1:38

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