theorem :: SCMPDS_4:14

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