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 ex K being Function of (Polish-WFF-set (L,E)),D st K is g -recursive
let E be Polish-arity-function of L; :: thesis: for D being non empty set
for g being Polish-recursion-function of E,D ex K being Function of (Polish-WFF-set (L,E)),D st K is g -recursive
let D be non empty set ; :: thesis: for g being Polish-recursion-function of E,D ex K being Function of (Polish-WFF-set (L,E)),D st K is g -recursive
let g be Polish-recursion-function of E,D; :: thesis: ex K being Function of (Polish-WFF-set (L,E)),D st K is g -recursive
set W = Polish-WFF-set (L,E);
defpred S₁[ object , object ] means ex n being Nat ex J1 being Subset of (Polish-WFF-set (L,E)) ex H1 being Function of J1,D st
( J1 = Polish-expression-hierarchy (L,E,n) & H1 is g -recursive & $1 in J1 & $2 = H1 . $1 );
A1: for a being object st a in Polish-WFF-set (L,E) holds
ex b being object st
( b in D & S₁[a,b] )

proof

let a be object ; :: thesis: ( a in Polish-WFF-set (L,E) implies ex b being object st
( b in D & S₁[a,b] ) )
assume a in Polish-WFF-set (L,E) ; :: thesis: ex b being object st
( b in D & S₁[a,b] )
then consider n being Nat such that
A2: a in Polish-expression-hierarchy (L,E,(n + 1)) by Th28;
consider J1 being Subset of (Polish-WFF-set (L,E)), H1 being Function of J1,D such that
A3: J1 = Polish-expression-hierarchy (L,E,(n + 1)) and
A4: H1 is g -recursive by Th74;
take b = H1 . a; :: thesis: ( b in D & S₁[a,b] )
thus b in D by A2, A3, FUNCT_2:5; :: thesis: S₁[a,b]
thus S₁[a,b] by A2, A3, A4; :: thesis: verum

end;

consider K being Function of (Polish-WFF-set (L,E)),D such that
A10: for a being object st a in Polish-WFF-set (L,E) holds
S₁[a,K . a] from FUNCT_2:sch 1(A1);
take K ; :: thesis: K is g -recursive
Polish-WFF-set (L,E) c= Polish-WFF-set (L,E) ;
then reconsider J = Polish-WFF-set (L,E) as Subset of (Polish-WFF-set (L,E)) ;
reconsider H = K as Function of J,D ;
A12: H is g -recursive by A10, Lm82;
let F be Polish-WFF of L,E; :: according to POLNOT_1:def 42 :: thesis: K . F = g . [(L -head F),(K * (Polish-WFF-args F))]
rng (Polish-WFF-args F) c= J by FINSEQ_1:def 4;
hence K . F = g . [(L -head F),(K * (Polish-WFF-args F))] by A12; :: thesis: verum