let ins be Element of the Instructions of Trivial-COM; :: thesis: InsCode ins = 0
the Instructions of Trivial-COM = {[0,{},{}]} by Def1;
then ins = [0,{},{}] by TARSKI:def 1;
hence InsCode ins = 0 by RECDEF_2:def 1; :: thesis: verum