theorem Th127: :: HILB10_7:127

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 Ee being Enumeration of Ext (F1,(1 + m),(2 + m)) st Ee = Ext (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 CFe 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 & CFe = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F1,(1 + (len f)),(2 + (len f)))))) * Ee holds
for Sd being Element of Fin (dom (App CFe)) st Sd = S holds
(M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1))) . ((len E1) |-> (1 + (len f))) = A $$ (Sd,(M "**" (App CFe))) ) )