let N be with_zero set ; :: thesis: for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0

let I be Instruction of (Trivial-AMI N); :: thesis: JumpPart I = 0

the InstructionsF of (Trivial-AMI N) = {[0,0,{}]} by EXTPRO_1:def 1;

then I = [0,0,0] by TARSKI:def 1;

hence JumpPart I = 0 ; :: thesis: verum

let I be Instruction of (Trivial-AMI N); :: thesis: JumpPart I = 0

the InstructionsF of (Trivial-AMI N) = {[0,0,{}]} by EXTPRO_1:def 1;

then I = [0,0,0] by TARSKI:def 1;

hence JumpPart I = 0 ; :: thesis: verum