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 A1: 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 consider x being set such that
A2: x in rng (ProgramPart p) by XBOOLE_0:def 1;
rng (ProgramPart p) c= the Instructions of S by RELAT_1:def 19;
hence halt S in rng (ProgramPart p) by A1, A2; :: 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
A3: i <> halt S ;
reconsider s = ( the State of S +* (NAT --> i)) +* p as State of S ;
A4: p c= s by FUNCT_4:26;
then B4: NPP p c= s by XBOOLE_1:1;
A5: ProgramPart p c= ProgramPart s by RELAT_1:105, FUNCT_4:26;
ProgramPart p c= ProgramPart s by A4, RELAT_1:105;
then ProgramPart s halts_on s by Def10, B4;
then consider k being Nat such that
IC (Comput ((ProgramPart s),s,k)) in dom (ProgramPart s) and
A6: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt S by Def7;
set m = IC (Comput ((ProgramPart s),s,k));
dom (ProgramPart s) = NAT by PARTFUN1:def 4;
then A7: (ProgramPart s) . (IC (Comput ((ProgramPart s),s,k))) = halt S by A6, PARTFUN1:def 8;

A8: now

assume not IC (Comput ((ProgramPart s),s,k)) in dom (ProgramPart p) ; :: thesis: contradiction
then A9: not IC (Comput ((ProgramPart s),s,k)) in dom p by RELAT_1:86;
A10: dom (NAT --> i) = NAT by FUNCOP_1:19;
(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 A9, FUNCT_4:12
.= (NAT --> i) . (IC (Comput ((ProgramPart s),s,k))) by A10, FUNCT_4:14
.= i by FUNCOP_1:13 ;
hence contradiction by A7, A3; :: thesis: verum

end;

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

end;

end;