theorem Th86: :: HILB10_7:86

for D being non empty set
for B being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp & 1 + (len f) in meet F & not 2 + (len f) in union F holds
B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,((the_inverseOp_wrt B) . d2)))*>),B,F)) * E)