let L be non trivial Polish-language; :: thesis: 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)*>)
let E be Polish-arity-function of L; :: thesis: 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)*>)
let D be non empty set ; :: thesis: 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)*>)
let g be Polish-recursion-function of E,D; :: thesis: 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)*>)
set W = Polish-WFF-set (L,E);
let K be Function of (Polish-WFF-set (L,E)),D; :: thesis: 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)*>)
let t be Element of L; :: thesis: 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)*>)
let F be Polish-WFF of L,E; :: thesis: ( K is g -recursive & E . t = 1 implies K . ((Polish-unOp (L,E,t)) . F) = g . (t,<*(K . F)*>) )
assume that
A1: K is g -recursive and
A2: E . t = 1 ; :: thesis: K . ((Polish-unOp (L,E,t)) . F) = g . (t,<*(K . F)*>)
set G = (Polish-unOp (L,E,t)) . F;
reconsider G1 = (Polish-unOp (L,E,t)) . F as Element of Polish-WFF-set (L,E) ;
A3: dom K = Polish-WFF-set (L,E) by FUNCT_2:def 1;
Polish-WFF-args G1 = <*F*> by A2, Th81;
then A5: K * (Polish-WFF-args G1) = <*(K . F)*> by A3, FINSEQ_2:34;
thus K . ((Polish-unOp (L,E,t)) . F) = g . [(L -head G1),(K * (Polish-WFF-args G1))] by A1
.= g . [t,(K * (Polish-WFF-args G1))] by A2, Th81
.= g . (t,<*(K . F)*>) by A5, BINOP_1:def 1 ; :: thesis: verum