let N be non empty with_non-empty_elements set ; :: thesis: for x being set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for i being Instruction of S holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) )
let x be set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for i being Instruction of S holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) )
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for i being Instruction of S holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) )
let i be Instruction of S; :: thesis: ( x in dom (Macro i) iff ( x = 0 or x = 1 ) )
dom (Macro i) = {0,1} by FUNCT_4:65;
hence ( x in dom (Macro i) iff ( x = 0 or x = 1 ) ) by TARSKI:def 2; :: thesis: verum