theorem Th26: :: COMPOS_2:26

for S being with_non_trivial_Instructions COM-Struct
for I being MacroInstruction of S
for k being Nat holds
( k < LastLoc I iff k in dom (CutLastLoc I) )