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