let I be non empty NAT -defined finite Function; :: thesis: (I,I)
thus CutLastLoc I c= I ; :: according to COMPOS_2:def 4 :: thesis: verum