let I be Instruction of Trivial-COM; :: thesis: JumpPart I = 0
the InstructionsF of Trivial-COM = {[0,0,0]} by Def1;
then I = [0,0,0] by TARSKI:def 1;
hence JumpPart I = 0 ; :: thesis: verum