theorem Th35: :: COMPOS_2:36

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