theorem :: COMPOS_2:42

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