reconsider v = a as Element of SCM-Data-Loc by Def2;
2 in {2,3} by TARSKI:def 2;
then [2,<*v,k1*>] in SCMPDS-Instr by Th18;
hence [2,<*a,k1*>] is Instruction of SCMPDS ; :: thesis: verum