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

now

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

A1: now

reconsider il1 = il as Element of ObjectKind (IC ) by MEMSTR_0:def 3;
reconsider n = il1 as Element of NAT ;
set I = goto i1;
set t = the State of SCM+FSA;
set Q = the Instruction-Sequence of SCM+FSA;
assume A2: x = i1 ; :: thesis: x in { (IC (Exec ((goto i1),s))) where s is Element of product the Object-Kind of SCM+FSA : IC s = il }
reconsider u = the State of SCM+FSA +* ((IC ),il1) as Element of product the Object-Kind of SCM+FSA by CARD_3:107;
reconsider P = the Instruction-Sequence of SCM+FSA +* (il,(goto i1)) as Instruction-Sequence of SCM+FSA ;
IC in dom the State of SCM+FSA by MEMSTR_0:2;
then A3: IC u = n by FUNCT_7:31;
A4: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of SCM+FSA by PARTFUN1:def 2;
then B4: P . n = goto i1 by FUNCT_7:31;
then IC (Following (P,u)) = i1 by A3, A4, SCMFSA_2:69;
hence x in { (IC (Exec ((goto i1),s))) where s is Element of product the Object-Kind of SCM+FSA : IC s = il } by A2, A3, B4, A4; :: thesis: verum

end;

now

assume x in { (IC (Exec ((goto i1),s))) where s is Element of product the Object-Kind of SCM+FSA : IC s = il } ; :: thesis: x = i1
then ex s being Element of product the Object-Kind of SCM+FSA st
( x = IC (Exec ((goto i1),s)) & IC s = il ) ;
hence x = i1 by SCMFSA_2:69; :: thesis: verum

end;

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

end;

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