let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for I, J being MacroInstruction of S holds I <= I ';' J
let I, J be MacroInstruction of S; :: thesis: I <= I ';' J
dom (CutLastLoc I) misses dom (Reloc (J,((card I) -' 1))) by COMPOS_1:18;
hence CutLastLoc I c= I ';' J by FUNCT_4:32; :: according to COMPOS_2:def 4 :: thesis: verum