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 (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM+FSA : ( IC s = il & (ProgramPart s) /. il = goto i1 ) } )

A1: now

reconsider il1 = il as Element of ObjectKind (IC SCM+FSA ) by AMI_1:def 11;
reconsider n = il1 as Element of NAT ;
reconsider I = goto i1 as Element of the Object-Kind of SCM+FSA . il by AMI_1:def 14;
consider t being State of SCM+FSA ;
assume A2: x = i1 ; :: thesis: x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM+FSA : ( IC s = il & (ProgramPart s) /. il = goto i1 ) }
reconsider p = (IC SCM+FSA ),il --> il1,I as PartState of SCM+FSA by AMI_1:149;
reconsider u = t +* p as Element of product the Object-Kind of SCM+FSA by PBOOLE:155;
A3: u . n = goto i1 by AMI_1:129;
X: (ProgramPart u) /. il = u . il by AMI_1:150;
A4: IC u = n by AMI_1:129;
then IC (Following (ProgramPart u),u) = i1 by A3, SCMFSA_2:95, X;
hence x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM+FSA : ( IC s = il & (ProgramPart s) /. il = goto i1 ) } by A2, A4, A3, X; :: thesis: verum

end;

now

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

end;

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

end;

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