theorem Th107: :: HILB10_7:107

for D being non empty set
for A being BinOp of D
for f, g 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 & len f <= len g holds
doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp (g,A,F2)) * E2)