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 holds
(I ';' J) . k = I . k
let I, J be MacroInstruction of S; :: thesis: for k being Nat st k < LastLoc I holds
(I ';' J) . k = I . k
let k be Nat; :: thesis: ( k < LastLoc I implies (I ';' J) . k = I . k )
assume k < LastLoc I ; :: thesis: (I ';' J) . k = I . k
then A1: k in dom (CutLastLoc I) by Th26;
dom (CutLastLoc I) misses dom (Reloc (J,((card I) -' 1))) by COMPOS_1:18;
then not k in dom (Reloc (J,((card I) -' 1))) by A1, XBOOLE_0:3;
hence (I ';' J) . k = (CutLastLoc I) . k by FUNCT_4:11
.= I . k by A1, GRFUNC_1:2 ;
:: thesis: verum