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