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