consider loc being Element of NAT ;
reconsider h = halt S as Element of the Object-Kind of S . loc by Def14;
reconsider l = loc as Element of NAT ;
K: dom ((IC S) .--> l) = {(IC S)} by FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in {(IC S)} implies ((IC S) .--> l) . x in the Object-Kind of S . x )
assume x in {(IC S)} ; :: thesis: ((IC S) .--> l) . x in the Object-Kind of S . x
then Z: x = IC S by TARSKI:def 1;
then A: ((IC S) .--> l) . x = l by FUNCOP_1:87;
ObjectKind (IC S) = NAT by Def11;
hence ((IC S) .--> l) . x in the Object-Kind of S . x by A, Z; :: thesis: verum

end;

then Y: ( (IC S) .--> l is the carrier of S -defined & (IC S) .--> l is the Object-Kind of S -compatible ) by RELAT_1:def 18, FUNCT_1:def 20, K;
U: l in NAT ;
NAT c= the carrier of S by Def3;
then T: {l} c= the carrier of S by ZFMISC_1:37, U;
L: dom (l .--> h) = {l} by FUNCOP_1:19;
V: dom (l .--> h) c= the carrier of S by T, FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in {l} implies (l .--> h) . x in the Object-Kind of S . x )
assume x in {l} ; :: thesis: (l .--> h) . x in the Object-Kind of S . x
then Z: x = loc by TARSKI:def 1;
then A: (l .--> h) . x = h by FUNCOP_1:87;
the Object-Kind of S . x = the Instructions of S by Z, Def14;
hence (l .--> h) . x in the Object-Kind of S . x by A; :: thesis: verum

end;

then ( l .--> h is the carrier of S -defined & l .--> h is the Object-Kind of S -compatible ) by RELAT_1:def 18, FUNCT_1:def 20, V, L;
then ( ((IC S) .--> l) +* (l .--> h) is the carrier of S -defined & ((IC S) .--> l) +* (l .--> h) is the Object-Kind of S -compatible ) by Y;
then reconsider p = (IC S),l --> l,(halt S) as FinPartState of S by FUNCT_4:def 4;
( p is autonomic & p is halting ) by Th65, Th67;
hence ex b₁ being FinPartState of S st
( b₁ is autonomic & b₁ is halting ) ; :: thesis: verum