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

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

end;

hence CutLastLoc I is halt-free ; :: thesis: verum