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