theorem Th49: :: COMPOS_2:50

for S being with_non_trivial_Instructions COM-Struct
for j being No-StopCode Instruction of S
for I being MacroInstruction of S holds (I ';' j) . (LastLoc I) = IncAddr (j,(LastLoc I))