let S be COM-Struct ; :: thesis: for i being Instruction of S holds (Macro i) . 1 = halt S
let i be Instruction of S; :: thesis: (Macro i) . 1 = halt S
A1: 0 in dom (Stop S) by Th3;
A2: (Stop S) . 0 = halt S by AFINSQ_1:34;
1 = 0 + (card (Load i)) by Th54;
hence (Macro i) . 1 = halt S by A2, A1, AFINSQ_1:def 3; :: thesis: verum