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