theorem Th113: :: HILB10_7:113

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for S being Element of Fin (dom (App ((SignGenOp (f,A,F)) * E))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (dom (App ((SignGenOp (f,A,F)) * (E * p))))