let s be State of (SCM R); :: according to AMISTD_1:def 16 :: thesis: (Exec (a := b),s) . (IC (SCM R)) = NextLoc (IC s),(SCM R)
succ (IC s) = NextLoc (IC s),(SCM R) by Th68;
hence (Exec (a := b),s) . (IC (SCM R)) = NextLoc (IC s),(SCM R) by SCMRING2:13; :: thesis: verum