theorem Th129: :: HILB10_7:129

for m being Nat
for D being non empty set
for A, M being BinOp of D
for F1 being finite set st A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is associative & M is commutative & M is having_a_unity & M is_distributive_wrt A holds
for E1 being Enumeration of F1 st union F1 c= Seg (1 + m) holds
for Es being Enumeration of swap (F1,(1 + m),(2 + m)) st Es = Swap (E1,(1 + m),(2 + m)) holds
ex S being Subset of (doms ((m + 2),(card F1))) st
( S = (len E1) -tuples_on {(1 + m),(2 + m)} & ( for CFs being non-empty non empty FinSequence of D *
for f being FinSequence of D
for d1, d2 being Element of D st len f = m & CFs = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap (F1,(1 + (len f)),(2 + (len f)))))) * Es holds
for Sd being Element of Fin (dom (App CFs)) st Sd = S holds
(M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F1)) * E1))) . ((len E1) |-> (1 + (len f))) = A $$ (Sd,(M "**" (App CFs))) ) )