:: deftheorem defines Polish-WFF-args POLNOT_1:def 39 :
for T being Polish-language
for A being Polish-arity-function of T
for F being Polish-WFF of T,A holds Polish-WFF-args F = decomp ((Polish-WFF-set (T,A)),(Polish-arity F),((T,A) -tail F));