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