let s be State of SCM; :: according to AMISTD_1:def 16 :: thesis: (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s)
thus (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) by AMI_3:11; :: thesis: verum