theorem :: COMPOS_2:3

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