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