theorem :: COMPOS_2:6

for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S
for K being MacroInstruction of S holds (i ';' j) ';' K = i ';' (j ';' K) by COMPOS_1:29;