for L being non trivial Polish-language
for E being Polish-arity-function of L
for D being non empty set
for g being Polish-recursion-function of E,D ex K being Function of (Polish-WFF-set (L,E)),D st K is g -recursive