theorem :: HILB10_7:95

for D being non empty set
for A, M being BinOp of D
for f, g being FinSequence of D
for F1 being finite set st A is having_a_unity & A is commutative & A is associative holds
for E1 being Enumeration of F1
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp ((f ^ g),A,F1)) * E1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S1 = S2 holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))