theorem :: SCMPDS_4:11

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