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