theorem :: SCMPDS_4:13

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