let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for K being MacroInstruction of S
for i1, i2, i3, i4 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' K) . 0 = i1
let K be MacroInstruction of S; :: thesis: for i1, i2, i3, i4 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' K) . 0 = i1
let i1, i2, i3, i4 be No-StopCode Instruction of S; :: thesis: ((((i1 ';' i2) ';' i3) ';' i4) ';' K) . 0 = i1
LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4 by Th32;
hence ((((i1 ';' i2) ';' i3) ';' i4) ';' K) . 0 = (((i1 ';' i2) ';' i3) ';' i4) . 0 by Th23, Th28
.= (((i1 ';' i2) ';' i3) ';' (Macro i4)) . 0
.= i1 by Th37 ;
:: thesis: verum