theorem :: SCMPDS_4:12

for j being Instruction of SCMPDS
for I, K being Program of holds (I ';' j) ';' K = I ';' (j ';' K) by AFINSQ_1:27;