theorem Th74: :: POLNOT_1:74

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
for n being Nat ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive )