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

hence
CutLastLoc I is halt-free
; :: thesis: verumassume
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;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