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 a being object st K is g -recursive & a in Polish-atoms (L,E) holds
K . a = g . (a,{})
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 a being object st K is g -recursive & a in Polish-atoms (L,E) holds
K . a = g . (a,{})
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 a being object st K is g -recursive & a in Polish-atoms (L,E) holds
K . a = g . (a,{})
let g be Polish-recursion-function of E,D; :: thesis: 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,{})
set W = Polish-WFF-set (L,E);
let K be Function of (Polish-WFF-set (L,E)),D; :: thesis: for a being object st K is g -recursive & a in Polish-atoms (L,E) holds
K . a = g . (a,{})
let a be object ; :: thesis: ( K is g -recursive & a in Polish-atoms (L,E) implies K . a = g . (a,{}) )
assume that
A1: K is g -recursive and
A2: a in Polish-atoms (L,E) ; :: thesis: K . a = g . (a,{})
reconsider F = a as Polish-WFF of L,E by A2, Th34, TARSKI:def 3;
A3: ( L -head F = F & Polish-WFF-args F = {} ) by A2, Th85;
thus K . a = g . [(L -head F),(K * (Polish-WFF-args F))] by A1
.= g . (F,(K * {})) by A3, BINOP_1:def 1
.= g . (a,{}) ; :: thesis: verum