theorem :: COMPOS_2:2

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