set S = Trivial-COM N;
halt (Trivial-COM N) = [0,{},{}] by Def2;
hence JumpPart (halt (Trivial-COM N)) is empty by RECDEF_2:def 2; :: according to COMPOS_1:def 37,COMPOS_1:def 39 :: thesis: verum