let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for I, J being MacroInstruction of S
for k being Nat st k < LastLoc I & I <= J holds
I . k = J . k
let I, J be MacroInstruction of S; :: thesis: for k being Nat st k < LastLoc I & I <= J holds
I . k = J . k
let k be Nat; :: thesis: ( k < LastLoc I & I <= J implies I . k = J . k )
assume Z1: k < LastLoc I ; :: thesis: ( not I <= J or I . k = J . k )
assume Z2: CutLastLoc I c= J ; :: according to COMPOS_2:def 4 :: thesis: I . k = J . k
B: k in dom (CutLastLoc I) by Z1, Th26;
thus I . k = (CutLastLoc I) . k by Z1, Th27
.= J . k by Z2, B, GRFUNC_1:2 ; :: thesis: verum