let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i being No-StopCode Instruction of S holds LastLoc (Macro i) = 1
let i be No-StopCode Instruction of S; :: thesis: LastLoc (Macro i) = 1
thus LastLoc (Macro i) = (card (Macro i)) - 1 by AFINSQ_1:91
.= 2 - 1 by COMPOS_1:56
.= 1 ; :: thesis: verum