theorem :: HILB10_7:142

for D being non empty set
for A, M being BinOp of D
for f being FinSequence of D st M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for E being Enumeration of bool {2}
for CE being non-empty non empty FinSequence of D * st CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 holds
ex S being Element of Fin (dom (App CE)) st
( S is with_evenly_repeated_values-member & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) )