let s be State of SCM+FSA; :: according to AMISTD_1:def 8 :: thesis: (Exec (((f,b) := a),s)) . (IC ) = succ (IC s)
thus (Exec (((f,b) := a),s)) . (IC ) = succ (IC s) by SCMFSA_2:73; :: thesis: verum