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 SCM+FSA) by COMPOS_1:def 6;
reconsider n = il1 as Element of NAT ;
reconsider I = goto i1 as Element of the Object-Kind of SCM+FSA . il by COMPOS_1:def 8;
consider t being State 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 p = ((IC SCM+FSA),il) --> (il1,I) as PartState of SCM+FSA by COMPOS_1:37;
reconsider u = t +* p as Element of product the Object-Kind of SCM+FSA by PBOOLE:155;
A4: IC u = n by EXTPRO_1:26;
IC (Exec ((goto i1),u)) = i1 by SCMFSA_2:95;
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, 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:95; :: 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:2; :: thesis: verum