InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence MultBy (a,b) is No-StopCode by COMPOS_0:def 12; :: thesis: verum