let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i being No-StopCode Instruction of S
for J being MacroInstruction of S holds (i ';' J) . 0 = i
let i be No-StopCode Instruction of S; :: thesis: for J being MacroInstruction of S holds (i ';' J) . 0 = i
let J be MacroInstruction of S; :: thesis: (i ';' J) . 0 = i
LastLoc (Macro i) = 1 by Th29;
hence (i ';' J) . 0 = (Macro i) . 0 by Th23, Th28
.= i by COMPOS_1:58 ;
:: thesis: verum