per cases
( InsCode I = 0 or InsCode I = 1 )
by AMISTD_1:6;

end;

suppose
InsCode I = 0
; :: thesis: JUMP I is empty

then
for f being Nat holds NIC (I,f) = {f}
by AMISTD_1:2, AMISTD_1:4;

hence JUMP I is empty by AMISTD_1:1; :: thesis: verum

end;hence JUMP I is empty by AMISTD_1:1; :: thesis: verum

suppose
InsCode I = 1
; :: thesis: JUMP I is empty

then
for f being Element of NAT holds NIC (I,f) = {(f + 1)}
by AMISTD_1:10;

hence JUMP I is empty by Th2; :: thesis: verum

end;hence JUMP I is empty by Th2; :: thesis: verum