theorem Th98: :: HILB10_7:98

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1
for g being Function st union F1 c= dom g & g | (union F1) is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)