let N be non empty with_non-empty_elements set ; :: thesis: for ins being Element of the Instructions of (Trivial-COM N) holds InsCode ins = 0
let ins be Element of the Instructions of (Trivial-COM N); :: thesis: InsCode ins = 0
the Instructions of (Trivial-COM N) = {[0,{},{}]} by Def2;
then ins = [0,{},{}] by TARSKI:def 1;
hence InsCode ins = 0 by RECDEF_2:def 1; :: thesis: verum