let R be good Ring; :: thesis: for il being Element of NAT holds NIC (halt (SCM R)),il = {il}
let il be Element of NAT ; :: thesis: NIC (halt (SCM R)),il = {il}

now

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

A1: now

reconsider il1 = il as Element of ObjectKind (IC (SCM R)) by AMI_1:def 11;
reconsider I = halt (SCM R) as Element of the Object-Kind of (SCM R) . il by AMI_1:def 14;
consider t being State of (SCM R);
assume A2: x = il ; :: thesis: x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of (SCM R) : ( IC s = il & (ProgramPart s) /. il = halt (SCM R) ) }
reconsider p = (IC (SCM R)),il --> il1,I as PartState of (SCM R) by AMI_1:149;
reconsider u = t +* p as Element of product the Object-Kind of (SCM R) by PBOOLE:155;
A3: dom ((IC (SCM R)),il --> il1,I) = {(IC (SCM R)),il} by FUNCT_4:65;
then il in dom ((IC (SCM R)),il --> il1,I) by TARSKI:def 2;
then A4: u . il = ((IC (SCM R)),il --> il1,I) . il by FUNCT_4:14
.= halt (SCM R) by FUNCT_4:66 ;
X: (ProgramPart u) /. il = u . il by AMI_1:150;
A5: IC (SCM R) in dom ((IC (SCM R)),il --> il1,I) by A3, TARSKI:def 2;
then A6: IC u = ((IC (SCM R)),il --> il1,I) . (IC (SCM R)) by FUNCT_4:14
.= il by AMI_1:48, FUNCT_4:66 ;
then IC (Following (ProgramPart u),u) = u . (IC (SCM R)) by A4, AMI_1:def 8, X
.= ((IC (SCM R)),il --> il1,I) . (IC (SCM R)) by A5, FUNCT_4:14
.= il by AMI_1:48, FUNCT_4:66 ;
hence x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of (SCM R) : ( IC s = il & (ProgramPart s) /. il = halt (SCM R) ) } by A2, A4, A6, X; :: thesis: verum

end;

now

assume x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of (SCM R) : ( IC s = il & (ProgramPart s) /. il = halt (SCM R) ) } ; :: thesis: x = il
then consider s being Element of product the Object-Kind of (SCM R) such that
W: ( x = IC (Following (ProgramPart s),s) & IC s = il & (ProgramPart s) /. il = halt (SCM R) ) ;
thus x = il by AMI_1:def 8, W; :: thesis: verum

end;

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

end;

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