:: deftheorem defines Polish-arity POLNOT_1:def 36 :
for T being Polish-language
for A being Polish-arity-function of T
for n being Nat
for F being Element of Polish-expression-hierarchy (T,A,n) holds Polish-arity F = A . (Polish-WFF-head F);