let S be COM-Struct ; :: thesis: for i being Instruction of S holds dom (Macro i) = {0,1}
let i be Instruction of S; :: thesis: dom (Macro i) = {0,1}
for x being object holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) ) by Th44;
hence dom (Macro i) = {0,1} by TARSKI:def 2; :: thesis: verum