theorem Th27: :: COMPOS_2:27

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