let R be good Ring; :: thesis: for l being Element of NAT
for i being Instruction of (SCM R) st ( for s being State of (SCM R) st IC s = l holds
(Exec (i,s)) . (IC ) = succ (IC s) ) holds
NIC (i,l) = {(succ l)}
let l be Element of NAT ; :: thesis: for i being Instruction of (SCM R) st ( for s being State of (SCM R) st IC s = l holds
(Exec (i,s)) . (IC ) = succ (IC s) ) holds
NIC (i,l) = {(succ l)}
let i be Instruction of (SCM R); :: thesis: ( ( for s being State of (SCM R) st IC s = l holds
(Exec (i,s)) . (IC ) = succ (IC s) ) implies NIC (i,l) = {(succ l)} )
set t = the State of (SCM R);
reconsider I = i as Element of the Object-Kind of (SCM R) . l by COMPOS_1:def 8;
assume A1: for s being State of (SCM R) st IC s = l holds
(Exec (i,s)) . (IC ) = succ (IC s) ; :: thesis: NIC (i,l) = {(succ l)}

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

let x be set ; :: thesis: ( x in NIC (i,l) implies x in {(succ l)} )
assume x in NIC (i,l) ; :: thesis: x in {(succ l)}
then consider s being Element of product the Object-Kind of (SCM R) such that
A2: ( x = IC (Exec (i,s)) & IC s = l ) ;
x = succ l by A1, A2;
hence x in {(succ l)} by TARSKI:def 1; :: thesis: verum

end;

reconsider il1 = l as Element of ObjectKind (IC ) by COMPOS_1:def 6;
reconsider p = ((IC ),l) --> (il1,I) as PartState of (SCM R) by COMPOS_1:37;
reconsider u = the State of (SCM R) +* p as Element of product the Object-Kind of (SCM R) by PBOOLE:155;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(succ l)} or x in NIC (i,l) )
A3: (ProgramPart u) /. l = u . l by COMPOS_1:38;
assume x in {(succ l)} ; :: thesis: x in NIC (i,l)
then A4: x = succ l by TARSKI:def 1;
A5: ( IC u = l & u . l = i ) by EXTPRO_1:29;
then IC (Following ((ProgramPart u),u)) = succ l by A1, A3;
hence x in NIC (i,l) by A4, A5, A3; :: thesis: verum