for f being Nat holds NIC (I,f) = {f} by AMISTD_1:2, AMISTD_1:17;
hence JUMP I is empty by AMISTD_1:1; :: thesis: verum