theorem :: POLNOT_1:86

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 K being Function of (Polish-WFF-set (L,E)),D
for a being object st K is g -recursive & a in Polish-atoms (L,E) holds
K . a = g . (a,{})