let N be with_zero set ; :: thesis: for i being Element of the InstructionsF of (Trivial-AMI N) holds InsCode i = 0

let i be Element of the InstructionsF of (Trivial-AMI N); :: thesis: InsCode i = 0

the InstructionsF of (Trivial-AMI N) = {[0,{},{}]} by EXTPRO_1:def 1;

then i = [0,{},{}] by TARSKI:def 1;

hence InsCode i = 0 ; :: thesis: verum

let i be Element of the InstructionsF of (Trivial-AMI N); :: thesis: InsCode i = 0

the InstructionsF of (Trivial-AMI N) = {[0,{},{}]} by EXTPRO_1:def 1;

then i = [0,{},{}] by TARSKI:def 1;

hence InsCode i = 0 ; :: thesis: verum