let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for I being MacroInstruction of S
for k being Nat st k < LastLoc I holds
(CutLastLoc I) . k = I . k
let I be MacroInstruction of S; :: thesis: for k being Nat st k < LastLoc I holds
(CutLastLoc I) . k = I . k
let k be Nat; :: thesis: ( k < LastLoc I implies (CutLastLoc I) . k = I . k )
assume k < LastLoc I ; :: thesis: (CutLastLoc I) . k = I . k
then A1: k in dom (CutLastLoc I) by Th26;
thus (CutLastLoc I) . k = I . k by A1, GRFUNC_1:2; :: thesis: verum