consider t being State of ;
let l be Instruction-Location of SCM ; :: thesis: for i being Instruction of st ( for s being State of st IC s = l & s . l = i holds
(Exec i,s) . (IC SCM ) = Next ) holds
NIC i,l = {(Next )}
let i be Instruction of ; :: thesis: ( ( for s being State of st IC s = l & s . l = i holds
(Exec i,s) . (IC SCM ) = Next ) implies NIC i,l = {(Next )} )
reconsider I = i as Element of ObjectKind l by AMI_1:def 14;
assume A1: for s being State of st IC s = l & s . l = i holds
(Exec i,s) . (IC SCM ) = Next ; :: thesis: NIC i,l = {(Next )}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(Next )} c= NIC i,l

let x be set ; :: thesis: ( x in NIC i,l implies x in {(Next )} )
assume x in NIC i,l ; :: thesis: x in {(Next )}
then ex s being State of st
( x = IC (Following s) & IC s = l & s . l = i ) ;
then x = Next by A1;
hence x in {(Next )} by TARSKI:def 1; :: thesis: verum

end;

l in NAT by AMI_1:def 4;
then reconsider il1 = l as Element of ObjectKind (IC SCM ) by AMI_1:def 11;
set u = t +* ((IC SCM ),l --> il1,I);
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Next )} or x in NIC i,l )
assume x in {(Next )} ; :: thesis: x in NIC i,l
then A2: x = Next by TARSKI:def 1;
A3: ( IC (t +* ((IC SCM ),l --> il1,I)) = l & (t +* ((IC SCM ),l --> il1,I)) . l = i ) by AMI_1:129;
then IC (Following (t +* ((IC SCM ),l --> il1,I))) = Next by A1;
hence x in NIC i,l by A2, A3; :: thesis: verum