let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over 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 with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over 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 :: thesis: for x being object holds
( x in {(NextLoc (il,S))} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } )

let x be object ; :: thesis: ( x in {(NextLoc (il,S))} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } )

A2: now :: thesis: ( x = NextLoc (il,S) implies x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } )

reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def 6;
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_Values_of S) : IC ss = il }
reconsider u = the State of S +* ((IC ),il1) as Element of product (the_Values_of S) by CARD_3:107;
il in NAT ;
then A4: il in dom the Instruction-Sequence of S by PARTFUN1:def 2;
A5: ( the Instruction-Sequence of S +* (il,i)) /. il = ( the Instruction-Sequence of S +* (il,i)) . il by PBOOLE:143
.= i by A4, FUNCT_7:31 ;
IC in dom the State of S by MEMSTR_0:2;
then A6: IC u = il by FUNCT_7:31;
then IC (Following (( the Instruction-Sequence of S +* (il,i)),u)) = NextLoc (il,S) by A1, A5;
hence x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } by A3, A6, A5; :: thesis: verum

end;

now :: thesis: ( x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } implies x = NextLoc (il,S) )

assume x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } ; :: thesis: x = NextLoc (il,S)
then ex s being Element of product (the_Values_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_Values_of S) : IC ss = il } ) by A2, TARSKI:def 1; :: thesis: verum

end;

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