theorem Th17: :: COMPOS_2:17
for F being non empty NAT -defined finite Function holds not LastLoc F in dom (CutLastLoc F)