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