theorem :: POLNOT_1:87

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 t being Element of L
for F being Polish-WFF of L,E st K is g -recursive & E . t = 1 holds
K . ((Polish-unOp (L,E,t)) . F) = g . (t,<*(K . F)*>)