theorem Th116: :: HILB10_7:116

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