for l being Element of NAT holds NIC ((MultBy (a,b)),l) = {(succ l)} by AMISTD_1:12;
hence JUMP (MultBy (a,b)) is empty by Lm2; :: thesis: verum