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;
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 A4: s c= s' ; :: thesis: R = (Result s') | (dom s)
h is halting by A1, A3, Def26;
then consider k1 being Element of NAT such that
A5: ( Result h = Computation h,k1 & CurInstr (Result h) = halt S ) by Def22;
s' is halting by A1, A4, Def26;
then consider k2 being Element of NAT such that
A6: ( Result s' = Computation s',k2 & 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 A5, Th52;
hence R = (Result s') | (dom s) by A1, A3, A4, A6, Def25; :: thesis: verum

end;

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

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

end;

end;

end;

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