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