thus not InsCode (b := f,a) is jump-only ; :: according to AMISTD_1:def 4 :: thesis: b := f,a is sequential
let s be State of SCM+FSA ; :: according to AMISTD_1:def 16 :: thesis: (Exec (b := f,a),s) . (IC SCM+FSA ) = NextLoc (IC s)
Next (IC s) = NextLoc (IC s) by Th88;
hence (Exec (b := f,a),s) . (IC SCM+FSA ) = NextLoc (IC s) by SCMFSA_2:98; :: thesis: verum