:: deftheorem defines Polish-recursion-domain POLNOT_1:def 41 :
for T being Polish-language
for A being Polish-arity-function of T
for D being non empty set holds Polish-recursion-domain (A,D) = { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } ;