let il be Element of NAT ; :: thesis: for k being natural number holds NIC ((SCM-goto k),il) = {k}
let k be natural number ; :: thesis: NIC ((SCM-goto k),il) = {k}

now

let x be set ; :: thesis: ( x in {k} iff x in { (IC (Exec ((SCM-goto k),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 ) by MEMSTR_0:def 3;
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 Object-Kind of SCM : IC s = il }
reconsider n = il as Element of NAT ;
reconsider u = the State of SCM +* ((IC ),il1) as Element of product the Object-Kind of SCM by CARD_3:107;
reconsider P = the Instruction-Sequence of SCM +* (il,(SCM-goto k)) as Instruction-Sequence of SCM ;
A3: P /. il = P . il 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 ;
then il in dom the Instruction-Sequence of SCM by PARTFUN1:def 2;
then B4: 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 Object-Kind of SCM : IC s = il } by A2, A4, A3, B4; :: thesis: verum

end;

now

assume x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product the Object-Kind of SCM : IC s = il } ; :: thesis: x = k
then ex s being Element of product the Object-Kind 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 Object-Kind of SCM : IC s = il } ) by A1, TARSKI:def 1; :: thesis: verum

end;

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