now :: thesis: not halt S in rng (CutLastLoc I)

assume halt S in rng (CutLastLoc I) ; :: thesis: contradiction
then consider x being set such that
W1: x in dom (CutLastLoc I) and
W2: (CutLastLoc I) . x = halt S by FUNCT_1:def 3;
dom (CutLastLoc I) c= dom I by RELAT_1:11;
then B: x in dom I by W1;
D: dom I c= NAT by RELAT_1:def 18;
I . x = halt S by W2, W1, GRFUNC_1:2;
then x = LastLoc I by B, D, COMPOS_1:def 15;
hence contradiction by W1, Th17; :: thesis: verum

end;

hence CutLastLoc I is halt-free by COMPOS_1:def 11; :: thesis: verum