per cases ( for i being Instruction of S holds i = halt S or ex i being Instruction of S st not i = halt S ) ;

suppose S: for i being Instruction of S holds i = halt S ; :: thesis: not ProgramPart p is halt-free

ProgramPart p <> {} by COMPOS_1:def 29;
then rng (ProgramPart p) <> {} ;
then consider x being set such that
W: x in rng (ProgramPart p) by XBOOLE_0:def 1;
rng (ProgramPart p) c= the Instructions of S by RELAT_1:def 19;
then x in the Instructions of S by W;
then x = halt S by S;
hence halt S in rng (ProgramPart p) by W; :: according to COMPOS_1:def 7 :: thesis: verum

end;

suppose not for i being Instruction of S holds i = halt S ; :: thesis: not ProgramPart p is halt-free

then consider i being Instruction of S such that
W0: i <> halt S ;
reconsider s = ( the State of S +* (NAT --> i)) +* p as State of S ;
W: p c= s by FUNCT_4:26;
then C: ProgramPart p c= ProgramPart s by RELAT_1:105;
ProgramPart s halts_on s by W, Def10;
then consider k being Nat such that
IC (Comput ((ProgramPart s),s,k)) in dom (ProgramPart s) and
W2: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt S by Def20;
set m = IC (Comput ((ProgramPart s),s,k));
dom (ProgramPart s) = NAT by PARTFUN1:def 4;
then IC (Comput ((ProgramPart s),s,k)) in dom (ProgramPart s) ;
then B: (ProgramPart s) . (IC (Comput ((ProgramPart s),s,k))) = (ProgramPart s) /. (IC (Comput ((ProgramPart s),s,k))) by PARTFUN1:def 8
.= halt S by W2 ;

A: now

assume not IC (Comput ((ProgramPart s),s,k)) in dom (ProgramPart p) ; :: thesis: contradiction
then A1: not IC (Comput ((ProgramPart s),s,k)) in dom p by RELAT_1:86;
dom (NAT --> i) = NAT by FUNCOP_1:19;
then A2: IC (Comput ((ProgramPart s),s,k)) in dom (NAT --> i) ;
(ProgramPart s) . (IC (Comput ((ProgramPart s),s,k))) = s . (IC (Comput ((ProgramPart s),s,k))) by COMPOS_1:2
.= ( the State of S +* (NAT --> i)) . (IC (Comput ((ProgramPart s),s,k))) by A1, FUNCT_4:12
.= (NAT --> i) . (IC (Comput ((ProgramPart s),s,k))) by A2, FUNCT_4:14
.= i by FUNCOP_1:13 ;
hence contradiction by B, W0; :: thesis: verum

end;

then (ProgramPart p) . (IC (Comput ((ProgramPart s),s,k))) = halt S by C, B, GRFUNC_1:8;
hence halt S in rng (ProgramPart p) by A, FUNCT_1:12; :: according to COMPOS_1:def 7 :: thesis: verum

end;

end;