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 A1: k < LastLoc I ; :: thesis: ( not I <= J or I . k = J . k )
assume A2: CutLastLoc I c= J ; :: according to COMPOS_2:def 4 :: thesis: I . k = J . k
A3: k in dom (CutLastLoc I) by A1, Th26;
thus I . k = (CutLastLoc I) . k by A1, Th27
.= J . k by A2, A3, GRFUNC_1:2 ; :: thesis: verum