reconsider v = a as Element of SCM-Data-Loc by AMI_2:def 16;
4 in {4,5,6,7,8} by ENUMSET1:def 3;
then [4,{},<*v,k1,k2*>] in SCMPDS-Instr by Th7;
hence [4,{},<*a,k1,k2*>] is Instruction of SCMPDS ; :: thesis: verum