theorem Th126: :: HILB10_7:126

for m being Nat
for D being non empty set
for A, M being BinOp of D
for F1, F2 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
for E2 being Enumeration of F2 st union F1 c= Seg (1 + m) & union F2 c= Seg (1 + m) holds
for Ee being Enumeration of Ext (F1,(1 + m),(2 + m))
for Es being Enumeration of swap (F2,(1 + m),(2 + m)) st Ee = Ext (E1,(1 + m),(2 + m)) & Es = Swap (E2,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F1,(1 + m),(2 + m))) \/ (swap (F2,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st s1 in doms ((m + 1),(card F1)) & s2 in doms ((m + 1),(card F2)) & s1 ^ s2 is with_evenly_repeated_values & card (s1 " {(1 + m)}) = card (s2 " {(1 + m)}) holds
ex S being Subset of (doms ((m + 2),((card F1) + (card F2)))) st
( ( card (s1 " {(1 + m)}) = 0 implies s1 ^ s2 in S ) & S is with_evenly_repeated_values-member & ( for CE1, CE2 being FinSequence of D *
for f being FinSequence of D
for d1, d2 being Element of D st len f = m & CE1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F2)) * E2 holds
for CFes being non-empty non empty FinSequence of D * st CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F1,(1 + (len f)),(2 + (len f)))) \/ (swap (F2,(1 + (len f)),(2 + (len f))))))) * Ees holds
for Sd being Element of Fin (dom (App CFes)) st S = Sd holds
( M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2)) = A $$ (Sd,(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in Sd & i in dom h holds
( ( (s1 ^ s2) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s1 ^ s2) . i <> 1 + (len f) implies h . i = (s1 ^ s2) . i ) ) ) ) ) )