reconsider h = halt S as Element of the Object-Kind of S . 0 by COMPOS_1:def 8;
K: dom ((IC S) .--> 0 ) = {(IC S)} by FUNCOP_1:19;

now

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

end;

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

now

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

end;

then ( 0 .--> h is the carrier of S -defined & 0 .--> h is the Object-Kind of S -compatible ) by V, L, FUNCT_1:def 20, RELAT_1:def 18;
then ( ((IC S) .--> 0 ) +* (0 .--> h) is the carrier of S -defined & ((IC S) .--> 0 ) +* (0 .--> h) is the Object-Kind of S -compatible ) by Y;
then reconsider p = (IC S),0 --> 0 ,(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