let s be State of (SCM R); :: according to AMISTD_1:def 8 :: thesis: (Exec ((SubFrom (a,b)),s)) . (0. (SCM R)) = succ (IC s)
thus (Exec ((SubFrom (a,b)),s)) . (0. (SCM R)) = succ (IC s) by SCMRING2:13; :: thesis: verum