let il, k be Nat; :: thesis: NIC ((SCM-goto k),il) = {k}

now :: thesis: for x being object holds
( x in {k} iff x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } )

let x be object ; :: thesis: ( x in {k} iff x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } )

A1: now :: thesis: ( x = k implies x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } )

il in NAT by ORDINAL1:def 12;
then reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def 6;
set I = SCM-goto k;
set t = the State of SCM;
set Q = the Instruction-Sequence of SCM;
assume A2: x = k ; :: thesis: x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il }
reconsider n = il as Element of NAT by ORDINAL1:def 12;
reconsider u = the State of SCM +* ((IC ),il1) as Element of product (the_Values_of SCM) by CARD_3:107;
reconsider P = the Instruction-Sequence of SCM +* (il,(SCM-goto k)) as Instruction-Sequence of SCM ;
reconsider ill = il as Element of NAT by ORDINAL1:def 12;
A3: P /. ill = P . ill by PBOOLE:143;
IC in dom the State of SCM by MEMSTR_0:2;
then A4: IC u = n by FUNCT_7:31;
il in NAT by ORDINAL1:def 12;
then il in dom the Instruction-Sequence of SCM by PARTFUN1:def 2;
then A5: P . n = SCM-goto k by FUNCT_7:31;
then IC (Following (P,u)) = k by A3, A4, AMI_3:7;
hence x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } by A2, A4, A3, A5; :: thesis: verum

end;

now :: thesis: ( x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } implies x = k )

assume x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } ; :: thesis: x = k
then ex s being Element of product (the_Values_of SCM) st
( x = IC (Exec ((SCM-goto k),s)) & IC s = il ) ;
hence x = k by AMI_3:7; :: thesis: verum

end;

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

end;

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