let S be COM-Struct ; :: thesis: for i being Instruction of S holds
( 0 in dom (Macro i) & 1 in dom (Macro i) )
let i be Instruction of S; :: thesis: ( 0 in dom (Macro i) & 1 in dom (Macro i) )
card (Macro i) = 2 by Th40;
hence ( 0 in dom (Macro i) & 1 in dom (Macro i) ) by AFINSQ_1:66; :: thesis: verum