let i be Instruction of SCM+FSA ; :: thesis: dom (Macro i) = {0 ,1}
for x being set holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) ) by SCMFSA6B:32;
hence dom (Macro i) = {0 ,1} by TARSKI:def 2; :: thesis: verum