for l being Instruction-Location of SCM R holds NIC (MultBy a,b),l = {(Next l)} by Th57;
hence JUMP (MultBy a,b) is empty by Lm6; :: thesis: verum