thus Trivial-AMI N is with_explicit_jumps :: thesis: verum

proof

let I be Instruction of (Trivial-AMI N); :: according to AMISTD_2:def 2 :: thesis: I is with_explicit_jumps
the InstructionsF of (Trivial-AMI N) = {[0,0,{}]} by EXTPRO_1:def 1;
then I = [0,0,0] by TARSKI:def 1;
hence JUMP I = rng (JumpPart I) ; :: according to AMISTD_2:def 1 :: thesis: verum

end;