theorem :: HILB10_7:94

for D being non empty set
for A being BinOp of D
for f, g being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1 holds doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp ((f ^ g),A,F1)) * E1)