theorem Th37: :: COMPOS_2:38

for S being with_non_trivial_Instructions COM-Struct
for i, j, k being No-StopCode Instruction of S
for K being MacroInstruction of S holds (((i ';' j) ';' k) ';' K) . 0 = i