for l being Nat holds NIC ((a := (f,b)),l) = {(l + 1)} by AMISTD_1:12;
hence JUMP (a := (f,b)) is empty by Lm1; :: thesis: verum