theorem Th99: :: HILB10_7:99

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 is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = (f * (g ")) | (dom fg) & 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
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) . (g * s)