theorem Th43: :: COMPOS_2:44

for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S
for j being Nat st j <= LastLoc J holds
(I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))