theorem Th117: :: HILB10_7:117

for D being non empty set
for A being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D st A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp holds
for F being non empty finite set st union F c= dom f holds
for F1, F2 being finite set st F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) holds
ex E1, E2 being Enumeration of F1 ex E being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F1)) * E2))