let R be good Ring; :: thesis: for i1, il being Instruction-Location of SCM R holds NIC (goto i1),il = {i1}
let i1, il be Instruction-Location of SCM R; :: 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 R) : ( 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 R) : ( IC s = il & s . il = goto i1 ) }
consider t being State of (SCM R);
il in NAT by AMI_1:def 4;
then reconsider il1 = il as Element of ObjectKind (IC (SCM R)) by AMI_1:def 11;
reconsider I = goto i1 as Element of ObjectKind il by AMI_1:def 14;
set u = t +* ((IC (SCM R)),il --> il1,I);
A3: dom ((IC (SCM R)),il --> il1,I) = {(IC (SCM R)),il} by FUNCT_4:65;
then A4: IC (SCM R) in dom ((IC (SCM R)),il --> il1,I) by TARSKI:def 2;
A5: IC (SCM R) <> il by AMI_1:48;
A6: IC (t +* ((IC (SCM R)),il --> il1,I)) = ((IC (SCM R)),il --> il1,I) . (IC (SCM R)) by A4, FUNCT_4:14
.= il by A5, FUNCT_4:66 ;
il in dom ((IC (SCM R)),il --> il1,I) by A3, TARSKI:def 2;
then A7: (t +* ((IC (SCM R)),il --> il1,I)) . il = ((IC (SCM R)),il --> il1,I) . il by FUNCT_4:14
.= goto i1 by FUNCT_4:66 ;
then IC (Following (t +* ((IC (SCM R)),il --> il1,I))) = i1 by A6, SCMRING2:17;
hence x in { (IC (Following s)) where s is State of (SCM R) : ( IC s = il & s . il = goto i1 ) } by A2, A6, A7; :: thesis: verum

end;

now

assume x in { (IC (Following s)) where s is State of (SCM R) : ( IC s = il & s . il = goto i1 ) } ; :: thesis: x = i1
then consider s being State of (SCM R) such that
A8: ( x = IC (Following s) & IC s = il & s . il = goto i1 ) ;
thus x = i1 by A8, SCMRING2:17; :: thesis: verum

end;

hence ( x in {i1} iff x in { (IC (Following s)) where s is State of (SCM R) : ( 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