let i be Instruction of SCMPDS ; :: thesis: for l being Element of NAT st ( for s being State of SCMPDS st IC s = l & s . l = i holds
(Exec i,s) . (IC SCMPDS ) = succ (IC s) ) holds
NIC i,l = {(succ l)}
let l be Element of NAT ; :: thesis: ( ( for s being State of SCMPDS st IC s = l & s . l = i holds
(Exec i,s) . (IC SCMPDS ) = succ (IC s) ) implies NIC i,l = {(succ l)} )
consider t being State of SCMPDS ;
reconsider I = i as Instruction of SCMPDS ;
reconsider n = l as Element of NAT ;
assume A1: for s being State of SCMPDS st IC s = l & s . l = i holds
(Exec i,s) . (IC SCMPDS ) = 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 SCMPDS such that
A2: x = IC (Following (ProgramPart s),s) and
A3: ( IC s = l & (ProgramPart s) /. l = i ) ;
X: (ProgramPart s) /. l = s . l by COMPOS_1:38;
Y: (ProgramPart s) . l = s . l by COMPOS_1:2;
x = (Exec ((ProgramPart s) . (IC s)),s) . (IC SCMPDS ) by A2, AMI_1:131
.= succ l by A1, A3, X, Y ;
hence x in {(succ l)} by TARSKI:def 1; :: thesis: verum

end;

reconsider il1 = l as Element of ObjectKind (IC SCMPDS ) by COMPOS_1:def 6;
(IC SCMPDS ),l --> il1,I = ((IC SCMPDS ) .--> il1) +* (l .--> I) by FUNCT_4:def 4;
then reconsider u = t +* ((IC SCMPDS ),l --> il1,i) as Element of product the Object-Kind of SCMPDS by PBOOLE:155;
A4: ( IC u = n & u . n = I ) by AMI_1:129;
X: (ProgramPart u) /. l = u . l by COMPOS_1:38;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(succ l)} or x in NIC i,l )
assume x in {(succ l)} ; :: thesis: x in NIC i,l
then A5: x = succ l by TARSKI:def 1;
IC (Following (ProgramPart u),u) = (Exec (u . (IC u)),u) . (IC SCMPDS ) by AMI_1:129
.= succ l by A1, A4 ;
hence x in NIC i,l by A5, A4, X; :: thesis: verum