consider h being State of S such that
A3: d c= h by PBOOLE:156;
ProgramPart h halts_on h by A1, A3, Def26;
then consider k1 being Element of NAT such that
A4: Result (ProgramPart h),h = Comput (ProgramPart h),h,k1 and
A5: CurInstr (ProgramPart h),(Result (ProgramPart h),h) = halt S by Def22;
reconsider R = (Result (ProgramPart h),h) | (dom d) as FinPartState of S ;
take R ; :: thesis: for s being State of S st d c= s holds
R = (Result (ProgramPart s),s) | (dom d)
let s be State of S; :: thesis: ( d c= s implies R = (Result (ProgramPart s),s) | (dom d) )
assume A6: d c= s ; :: thesis: R = (Result (ProgramPart s),s) | (dom d)
ProgramPart s halts_on s by A1, A6, Def26;
then consider k2 being Element of NAT such that
A7: Result (ProgramPart s),s = Comput (ProgramPart s),s,k2 and
A8: CurInstr (ProgramPart s),(Result (ProgramPart s),s) = halt S by Def22;

now

per cases ( k1 <= k2 or k1 >= k2 ) ;

suppose k1 <= k2 ; :: thesis: R = (Result (ProgramPart s),s) | (dom d)

then Result (ProgramPart h),h = Comput (ProgramPart h),h,k2 by A4, A5, Th52;
hence R = (Result (ProgramPart s),s) | (dom d) by A1, A3, A6, A7, Def25; :: thesis: verum

end;

suppose k1 >= k2 ; :: thesis: R = (Result (ProgramPart s),s) | (dom d)

then Result (ProgramPart s),s = Comput (ProgramPart s),s,k1 by A7, A8, Th52;
hence R = (Result (ProgramPart s),s) | (dom d) by A1, A3, A6, A4, Def25; :: thesis: verum

end;

end;

end;

hence R = (Result (ProgramPart s),s) | (dom d) ; :: thesis: verum