theorem Th90: :: HILB10_7:90

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 & ( for i being Nat st i in dom E1 holds
(dom f) /\ (E1 . i) = (dom f) /\ (E2 . i) ) holds
(SignGenOp (f,A,F1)) * E1 = (SignGenOp (f,A,F2)) * E2