theorem :: SCMPDS_4:15

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