let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i, j, k being No-StopCode Instruction of S
for K being MacroInstruction of S holds (((i ';' j) ';' k) ';' K) . 0 = i
let i, j, k be No-StopCode Instruction of S; :: thesis: for K being MacroInstruction of S holds (((i ';' j) ';' k) ';' K) . 0 = i
let K be MacroInstruction of S; :: thesis: (((i ';' j) ';' k) ';' K) . 0 = i
LastLoc ((i ';' j) ';' k) = 3 by Th31;
hence (((i ';' j) ';' k) ';' K) . 0 = ((i ';' j) ';' k) . 0 by Th23, Th28
.= ((i ';' j) ';' (Macro k)) . 0
.= i by Th36 ;
:: thesis: verum