consider h being Function such that
A2: h in product the Object-Kind of S and
A3: s c= h by CARD_3:70;
reconsider h = h as State of S by A2;
ProgramPart h halts_on h by A1, A3, Def26;
then consider k1 being Element of NAT such that
A4: Result h = Computation h,k1 and
A5: CurInstr (Result h) = halt S by Def22;
reconsider R = (Result h) | (dom s) as FinPartState of S by Th62;
take R ; :: thesis: for s' being State of S st s c= s' holds
R = (Result s') | (dom s)
let s' be State of S; :: thesis: ( s c= s' implies R = (Result s') | (dom s) )
assume A6: s c= s' ; :: thesis: R = (Result s') | (dom s)
ProgramPart s' halts_on s' by A1, A6, Def26;
then consider k2 being Element of NAT such that
A7: Result s' = Computation s',k2 and
A8: CurInstr (Result s') = halt S by Def22;

now

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

suppose k1 <= k2 ; :: thesis: R = (Result s') | (dom s)

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

end;

suppose k1 >= k2 ; :: thesis: R = (Result s') | (dom s)

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

end;

end;

end;

hence R = (Result s') | (dom s) ; :: thesis: verum