theorem :: SCMPDS_7:52

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for n being Nat holds (IExec ((sum n),P,s)) . (intpos 3) = n