reconsider I = i as Element of SCM+FSA-Data-Loc by Def4;
reconsider A = a as Element of SCM+FSA-Data*-Loc by Def5;
12 in {11,12} by TARSKI:def 2;
then [12,<*I,A*>] in SCM+FSA-Instr by SCMFSA_1:7;
hence [12,<*i,a*>] is Instruction of SCM+FSA ; :: thesis: verum