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 n being Nat
for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive holds
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 + 1)) & H1 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
for n being Nat
for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive holds
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 + 1)) & H1 is g -recursive )
let D be non empty set ; :: thesis: for g being Polish-recursion-function of E,D
for n being Nat
for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive holds
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 + 1)) & H1 is g -recursive )
let g be Polish-recursion-function of E,D; :: thesis: for n being Nat
for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive holds
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 + 1)) & H1 is g -recursive )
let n be Nat; :: thesis: for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive holds
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 + 1)) & H1 is g -recursive )
let J be Subset of (Polish-WFF-set (L,E)); :: thesis: for H being Function of J,D st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive holds
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 + 1)) & H1 is g -recursive )
let H be Function of J,D; :: thesis: ( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive implies 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 + 1)) & H1 is g -recursive ) )
assume that
A1: J = Polish-expression-hierarchy (L,E,n) and
A2: H is g -recursive ; :: thesis: 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 + 1)) & H1 is g -recursive )
set J1 = Polish-expression-hierarchy (L,E,(n + 1));
reconsider J1 = Polish-expression-hierarchy (L,E,(n + 1)) as Subset of (Polish-WFF-set (L,E)) by Th26;
defpred S₁[ object , object ] means ex F being Polish-WFF of L,E st
( F = $1 & $2 = g . [(L -head F),(H * (Polish-WFF-args F))] );
A4: for a being object st a in J1 holds
ex b being object st
( b in D & S₁[a,b] )

proof

let a be object ; :: thesis: ( a in J1 implies ex b being object st
( b in D & S₁[a,b] ) )
assume A5: a in J1 ; :: thesis: ex b being object st
( b in D & S₁[a,b] )
then reconsider F = a as Polish-WFF of L,E ;
set t = Polish-WFF-head F;
set q = Polish-WFF-args F;
rng (Polish-WFF-args F) c= J by A1, A5, Th71;
then reconsider q = Polish-WFF-args F as FinSequence of J by FINSEQ_1:def 4;
reconsider p = H * q as FinSequence of D by FINSEQ_2:32;
set c = [(Polish-WFF-head F),p];
take b = g . [(Polish-WFF-head F),p]; :: thesis: ( b in D & S₁[a,b] )
len p = len q by FINSEQ_2:33
.= E . (Polish-WFF-head F) by Th62 ;
then [(Polish-WFF-head F),p] in Polish-recursion-domain (E,D) ;
hence b in D by FUNCT_2:5; :: thesis: S₁[a,b]
thus S₁[a,b] ; :: thesis: verum

end;

consider H1 being Function of J1,D such that
A21: for a being object st a in J1 holds
S₁[a,H1 . a] from FUNCT_2:sch 1(A4);
take J1 ; :: thesis: ex H1 being Function of J1,D st
( J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H1 is g -recursive )
take H1 ; :: thesis: ( J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H1 is g -recursive )
thus J1 = Polish-expression-hierarchy (L,E,(n + 1)) ; :: thesis: H1 is g -recursive
for F being Polish-WFF of L,E st F in J1 holds
H1 . F = g . [(L -head F),(H * (Polish-WFF-args F))]

proof

let F be Polish-WFF of L,E; :: thesis: ( F in J1 implies H1 . F = g . [(L -head F),(H * (Polish-WFF-args F))] )
assume F in J1 ; :: thesis: H1 . F = g . [(L -head F),(H * (Polish-WFF-args F))]
then consider G being Polish-WFF of L,E such that
A41: G = F and
A42: H1 . F = g . [(L -head G),(H * (Polish-WFF-args G))] by A21;
thus H1 . F = g . [(L -head F),(H * (Polish-WFF-args F))] by A41, A42; :: thesis: verum

end;

hence H1 is g -recursive by A1, A2, Lm73; :: thesis: verum