theorem :: POLNOT_1:31

for X being set
for B being disjoint_valued FinSequence of bool X
for a being object
for n being Nat st a in B . n holds
(arity-from-list B) . a = n