theorem Th80: :: HILB10_7:80

for i being Nat
for D being non empty set
for B being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st ( i in dom E or i in dom ((SignGenOp (f,B,F)) * E) ) holds
((SignGenOp (f,B,F)) * E) . i = SignGen (f,B,(E . i))