let S be COM-Struct ; :: thesis: for x being set
for i being Instruction of S holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) )
let x be set ; :: 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 ) )
set si = Macro i;
set A = NAT ;
A1: card (Macro i) = 2 by Th40;
hereby :: thesis: ( ( x = 0 or x = 1 ) implies x in dom (Macro i) )
assume A2: x in dom (Macro i) ; :: thesis: ( x = 0 or x = 1 )
reconsider l = x as Element of NAT by A2;
reconsider n = l as Element of NAT ;
n < 1 + 1 by A1, A2, AFINSQ_1:66;
then n <= 1 by NAT_1:13;
hence ( x = 0 or x = 1 ) by NAT_1:25; :: thesis: verum
end;
thus ( ( x = 0 or x = 1 ) implies x in dom (Macro i) ) by A1, AFINSQ_1:66; :: thesis: verum