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