theorem :: HILB10_7:108

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 holds
doms ((SignGenOp (f,A,F1)) * E1) = doms ((SignGenOp (f,A,F2)) * E2)