:: deftheorem Def22 defines arity-from-list POLNOT_1:def 14 :
for X being set
for B being V107() FinSequence of bool X
for b₃ being Function of X,NAT holds
( b₃ = arity-from-list B iff for a being object holds
( not a in X or ( ex n being Nat st a in B . n & a in B . (b₃ . a) ) or ( ( for n being Nat holds not a in B . n ) & b₃ . a = 0 ) ) );