:: deftheorem Def2 defines Polish-arity-like POLNOT_2:def 2 :
for F being Function holds
( F is Polish-arity-like iff ( dom F is Polish-language & F is natural-valued & F is with_zero ) );