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