theorem :: SCMPDS_4:17

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