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 F1, F2 being Polish-WFF of L,E st K is g -recursive & E . t = 2 holds
K . ((Polish-binOp (L,E,t)) . (F1,F2)) = g . (t,<*(K . F1),(K . F2)*>)
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 F1, F2 being Polish-WFF of L,E st K is g -recursive & E . t = 2 holds
K . ((Polish-binOp (L,E,t)) . (F1,F2)) = g . (t,<*(K . F1),(K . F2)*>)
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 F1, F2 being Polish-WFF of L,E st K is g -recursive & E . t = 2 holds
K . ((Polish-binOp (L,E,t)) . (F1,F2)) = g . (t,<*(K . F1),(K . F2)*>)
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 F1, F2 being Polish-WFF of L,E st K is g -recursive & E . t = 2 holds
K . ((Polish-binOp (L,E,t)) . (F1,F2)) = g . (t,<*(K . F1),(K . F2)*>)
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 F1, F2 being Polish-WFF of L,E st K is g -recursive & E . t = 2 holds
K . ((Polish-binOp (L,E,t)) . (F1,F2)) = g . (t,<*(K . F1),(K . F2)*>)
let t be Element of L; :: thesis: for F1, F2 being Polish-WFF of L,E st K is g -recursive & E . t = 2 holds
K . ((Polish-binOp (L,E,t)) . (F1,F2)) = g . (t,<*(K . F1),(K . F2)*>)
let F1, F2 be Polish-WFF of L,E; :: thesis: ( K is g -recursive & E . t = 2 implies K . ((Polish-binOp (L,E,t)) . (F1,F2)) = g . (t,<*(K . F1),(K . F2)*>) )
assume that
A1: K is g -recursive and
A2: E . t = 2 ; :: thesis: K . ((Polish-binOp (L,E,t)) . (F1,F2)) = g . (t,<*(K . F1),(K . F2)*>)
set G = (Polish-binOp (L,E,t)) . (F1,F2);
reconsider G1 = (Polish-binOp (L,E,t)) . (F1,F2) as Element of Polish-WFF-set (L,E) ;
Polish-WFF-args G1 = <*F1,F2*> by A2, Th83;
then A5: K * (Polish-WFF-args G1) = <*(K . F1),(K . F2)*> by FINSEQ_2:36;
thus K . ((Polish-binOp (L,E,t)) . (F1,F2)) = g . [(L -head G1),(K * (Polish-WFF-args G1))] by A1
.= g . [t,(K * (Polish-WFF-args G1))] by A2, Th83
.= g . (t,<*(K . F1),(K . F2)*>) by A5, BINOP_1:def 1 ; :: thesis: verum