let i1, il be Instruction-Location of SCM+FSA ; :: thesis: NIC (goto i1),il = {i1}

now

let x be set ; :: thesis: ( x in {i1} iff x in { (IC (Following s)) where s is State of SCM+FSA : ( IC s = il & s . il = goto i1 ) } )

A1: now

assume A2: x = i1 ; :: thesis: x in { (IC (Following s)) where s is State of SCM+FSA : ( IC s = il & s . il = goto i1 ) }
consider t being State of SCM+FSA ;
il in NAT by AMI_1:def 4;
then reconsider il1 = il as Element of ObjectKind (IC SCM+FSA ) by AMI_1:def 11;
reconsider I = goto i1 as Element of ObjectKind il by AMI_1:def 14;
set u = t +* ((IC SCM+FSA ),il --> il1,I);
A3: IC (t +* ((IC SCM+FSA ),il --> il1,I)) = il by AMI_1:129;
A4: (t +* ((IC SCM+FSA ),il --> il1,I)) . il = goto i1 by AMI_1:129;
then IC (Following (t +* ((IC SCM+FSA ),il --> il1,I))) = i1 by A3, SCMFSA_2:95;
hence x in { (IC (Following s)) where s is State of SCM+FSA : ( IC s = il & s . il = goto i1 ) } by A2, A3, A4; :: thesis: verum

end;

now

assume x in { (IC (Following s)) where s is State of SCM+FSA : ( IC s = il & s . il = goto i1 ) } ; :: thesis: x = i1
then consider s being State of SCM+FSA such that
A5: ( x = IC (Following s) & IC s = il & s . il = goto i1 ) ;
thus x = i1 by A5, SCMFSA_2:95; :: thesis: verum

end;

hence ( x in {i1} iff x in { (IC (Following s)) where s is State of SCM+FSA : ( IC s = il & s . il = goto i1 ) } ) by A1, TARSKI:def 1; :: thesis: verum

end;

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