theorem :: COMPOS_2:43

for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S holds LastLoc (I ';' J) = (LastLoc I) + (LastLoc J)