theorem :: AMISTD_1:18

for N being with_zero set
for i being Element of the InstructionsF of (Trivial-AMI N) holds InsCode i = 0