theorem Th100: :: HILB10_7:100

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 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)))