reconsider A = a as Element of SCM+FSA-Data*-Loc by Def5;
reconsider C = c, I = i as Element of SCM+FSA-Data-Loc by Def4;
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