let il be Instruction-Location of SCM ; :: thesis: for k being natural number holds NIC (goto k),il = {k}
let k be natural number ; :: thesis: NIC (goto k),il = {k}

now

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

A1: now

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

end;

now

assume x in { (IC (Following s)) where s is State of : ( IC s = il & s . il = goto k ) } ; :: thesis: x = k
then ex s being State of st
( x = IC (Following s) & IC s = il & s . il = goto k ) ;
hence x = k by AMI_3:13; :: thesis: verum

end;

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

end;

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