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

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