reconsider a = a as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider loc = loc as Nat ;
8 in {7,8} by TARSKI:def 2;
then [8,<*loc*>,<*a*>] in SCM-Instr by SCM_INST:3;
hence [8,<*loc*>,<*a*>] is Instruction of SCM ; :: thesis: verum