theorem
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
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)*>)