theorem Th139: :: HILB10_7:139

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