let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated weakly_standard AMI-Struct of N
for il being Element of NAT
for i being Instruction of S st i is sequential holds
NIC (i,il) = {(NextLoc (il,S))}
let S be non empty IC-Ins-separated weakly_standard AMI-Struct of N; :: thesis: for il being Element of NAT
for i being Instruction of S st i is sequential holds
NIC (i,il) = {(NextLoc (il,S))}
let il be Element of NAT ; :: thesis: for i being Instruction of S st i is sequential holds
NIC (i,il) = {(NextLoc (il,S))}
let i be Instruction of S; :: thesis: ( i is sequential implies NIC (i,il) = {(NextLoc (il,S))} )
assume A1: for s being State of S holds (Exec (i,s)) . (IC ) = NextLoc ((IC s),S) ; :: according to AMI_WSTD:def 8 :: thesis: NIC (i,il) = {(NextLoc (il,S))}

now

let x be set ; :: thesis: ( x in {(NextLoc (il,S))} iff x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il } )

A2: now

reconsider il1 = il as Element of ObjectKind (IC ) by MEMSTR_0:def 3;
set I = i;
set t = the State of S;
set P = the Instruction-Sequence of S;
assume A3: x = NextLoc (il,S) ; :: thesis: x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il }
reconsider u = the State of S +* ((IC ),il1) as Element of product the Object-Kind of S by CARD_3:107;
il in NAT ;
then X: il in dom the Instruction-Sequence of S by PARTFUN1:def 2;
A6: ( the Instruction-Sequence of S +* (il,i)) /. il = ( the Instruction-Sequence of S +* (il,i)) . il by PBOOLE:143
.= i by X, FUNCT_7:31 ;
IC in dom the State of S by MEMSTR_0:2;
then A7: IC u = il by FUNCT_7:31;
then IC (Following (( the Instruction-Sequence of S +* (il,i)),u)) = NextLoc (il,S) by A1, A6;
hence x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il } by A3, A7, A6; :: thesis: verum

end;

now

assume x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il } ; :: thesis: x = NextLoc (il,S)
then ex s being Element of product the Object-Kind of S st
( x = IC (Exec (i,s)) & IC s = il ) ;
hence x = NextLoc (il,S) by A1; :: thesis: verum

end;

hence ( x in {(NextLoc (il,S))} iff x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il } ) by A2, TARSKI:def 1; :: thesis: verum

end;

hence NIC (i,il) = {(NextLoc (il,S))} by TARSKI:1; :: thesis: verum