theorem Th28: :: COMPOS_2:28

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