let s be State of (SCM R); :: according to AMISTD_1:def 16 :: thesis: (Exec (a := r),s) . (IC (SCM R)) = succ (IC s)
thus (Exec (a := r),s) . (IC (SCM R)) = succ (IC s) by SCMRING2:19; :: thesis: verum