theorem Th102: :: HILB10_7:102

for n being Nat
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 n in dom f holds
(len E1) |-> n in doms ((SignGenOp (f,A,F1)) * E1)