theorem :: COMPOS_2:1

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