let it1, it2 be Element of D; :: thesis: ( ( for E being Enumeration of bool F holds it1 = M $$ (([#] (dom ((SignGenOp (f,A,(bool F))) * E))),(A "**" ((SignGenOp (f,A,(bool F))) * E))) ) & ( for E being Enumeration of bool F holds it2 = M $$ (([#] (dom ((SignGenOp (f,A,(bool F))) * E))),(A "**" ((SignGenOp (f,A,(bool F))) * E))) ) implies it1 = it2 )
assume that
A10: for E being Enumeration of bool F holds it1 = M $$ (([#] (dom ((SignGenOp (f,A,(bool F))) * E))),(A "**" ((SignGenOp (f,A,(bool F))) * E))) and
A11: for E being Enumeration of bool F holds it2 = M $$ (([#] (dom ((SignGenOp (f,A,(bool F))) * E))),(A "**" ((SignGenOp (f,A,(bool F))) * E))) ; :: thesis: it1 = it2
set E = the Enumeration of bool F;
it1 = M $$ (([#] (dom ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F))),(A "**" ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F))) by A10;
hence it1 = it2 by A11; :: thesis: verum