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