let S be COM-Struct ; :: thesis: for i being Instruction of S holds (Macro i) . 0 = i
let i be Instruction of S; :: thesis: (Macro i) . 0 = i
set I = Load i;
0 in dom (Load i) by Th37;
hence (Macro i) . 0 = (Load i) . 0 by AFINSQ_1:def 3
.= i ;
:: thesis: verum