let il be Element of NAT ; :: thesis: NIC ((halt SCM),il) = {il}

now

let x be set ; :: thesis: ( x in {il} iff x in { (IC (Exec ((halt SCM),s))) where s is Element of product the Object-Kind of SCM : IC s = il } )

A1: now

reconsider il1 = il as Element of ObjectKind (IC SCM) by COMPOS_1:def 6;
reconsider I = halt SCM as Element of the Object-Kind of SCM . il by COMPOS_1:def 8;
consider t being State of SCM;
assume A2: x = il ; :: thesis: x in { (IC (Exec ((halt SCM),s))) where s is Element of product the Object-Kind of SCM : IC s = il }
reconsider p = ((IC SCM),il) --> (il1,I) as PartState of SCM by COMPOS_1:37;
reconsider u = t +* p as Element of product the Object-Kind of SCM by PBOOLE:155;
reconsider n = il as Element of NAT ;
dom (((IC SCM),il) --> (il1,I)) = {(IC SCM),il} by FUNCT_4:65;
then A3: IC SCM in dom (((IC SCM),il) --> (il1,I)) by TARSKI:def 2;
X: (ProgramPart u) /. il = u . il by COMPOS_1:38;
A4: ( u . n = halt SCM & IC u = n ) by EXTPRO_1:26;
then IC (Following ((ProgramPart u),u)) = u . (IC SCM) by X, EXTPRO_1:def 3
.= (((IC SCM),il) --> (il1,I)) . (IC SCM) by A3, FUNCT_4:14
.= il by COMPOS_1:3, FUNCT_4:66 ;
hence x in { (IC (Exec ((halt SCM),s))) where s is Element of product the Object-Kind of SCM : IC s = il } by A2, A4, X; :: thesis: verum

end;

now

assume x in { (IC (Exec ((halt SCM),s))) where s is Element of product the Object-Kind of SCM : IC s = il } ; :: thesis: x = il
then ex s being Element of product the Object-Kind of SCM st
( x = IC (Exec ((halt SCM),s)) & IC s = il ) ;
hence x = il by EXTPRO_1:def 3; :: thesis: verum

end;

hence ( x in {il} iff x in { (IC (Exec ((halt SCM),s))) where s is Element of product the Object-Kind of SCM : IC s = il } ) by A1, TARSKI:def 1; :: thesis: verum

end;

hence NIC ((halt SCM),il) = {il} by TARSKI:2; :: thesis: verum