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