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