:: deftheorem Def11 defines SignGen HILB10_7:def 11 :
for D being non empty set
for B being BinOp of D
for f being FinSequence of D
for X being set
for b₅ being FinSequence of D holds
( b₅ = SignGen (f,B,X) iff ( dom b₅ = dom f & ( for i being Nat st i in dom b₅ holds
( ( i in X implies b₅ . i = (the_inverseOp_wrt B) . (f . i) ) & ( not i in X implies b₅ . i = f . i ) ) ) ) );