theorem Th30: :: POLNOT_1:30

for X being set
for B being disjoint_valued FinSequence of bool X
for a being object st a in X holds
( (arity-from-list B) . a <> 0 iff ex n being Nat st a in B . n )