theorem Th81: :: HILB10_7:81

for D being non empty set
for B 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
for E12 being Enumeration of F1 \/ F2 st E12 = E1 ^ E2 holds
(SignGenOp (f,B,(F1 \/ F2))) * E12 = ((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)