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