:: deftheorem Def9 defines SgnMembershipNumber POLYNOM9:def 9 :
for f being finite Function
for L being doubleLoopStr
for E being Function
for b₄ being Element of L holds
( b₄ = SgnMembershipNumber (f,L,E) iff for c being Nat st c = card { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } holds
( ( c is even implies b₄ = 1. L ) & ( c is odd implies b₄ = - (1. L) ) ) );