:: deftheorem Def5 defines Polish-arity-function POLNOT_1:def 18 :
for T being Polish-language
for b₂ being Function of T,NAT holds
( b₂ is Polish-arity-function of T iff ex a being object st
( a in T & b₂ . a = 0 ) );