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 Th2;
A2: (Stop S) . 0 = halt S ;
1 = 0 + (card (Load i)) by Th38;
hence (Macro i) . 1 = halt S by A2, A1, AFINSQ_1:def 3; :: thesis: verum