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 J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D st ( for a being object st a in J holds
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 & a in J1 & H . a = H1 . a ) ) holds
H 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 J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D st ( for a being object st a in J holds
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 & a in J1 & H . a = H1 . a ) ) holds
H is g -recursive
let D be non empty set ; :: thesis: for g being Polish-recursion-function of E,D
for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D st ( for a being object st a in J holds
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 & a in J1 & H . a = H1 . a ) ) holds
H is g -recursive
let g be Polish-recursion-function of E,D; :: thesis: for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D st ( for a being object st a in J holds
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 & a in J1 & H . a = H1 . a ) ) holds
H is g -recursive
let J be Subset of (Polish-WFF-set (L,E)); :: thesis: for H being Function of J,D st ( for a being object st a in J holds
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 & a in J1 & H . a = H1 . a ) ) holds
H is g -recursive
let H be Function of J,D; :: thesis: ( ( for a being object st a in J holds
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 & a in J1 & H . a = H1 . a ) ) implies H is g -recursive )
assume A1: for a being object st a in J holds
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 & a in J1 & H . a = H1 . a ) ; :: thesis: H is g -recursive
let F be Polish-WFF of L,E; :: according to POLNOT_1:def 43 :: thesis: ( F in J & rng (Polish-WFF-args F) c= J implies H . F = g . [(L -head F),(H * (Polish-WFF-args F))] )
assume that
A10: F in J and
A11: rng (Polish-WFF-args F) c= J ; :: thesis: H . F = g . [(L -head F),(H * (Polish-WFF-args F))]
consider n being Nat, J1 being Subset of (Polish-WFF-set (L,E)), H1 being Function of J1,D such that
A12: J1 = Polish-expression-hierarchy (L,E,n) and
A13: H1 is g -recursive and
A14: F in J1 and
A15: H . F = H1 . F by A1, A10;
set J2 = Polish-expression-hierarchy (L,E,(n + 1));
set X = rng (Polish-WFF-args F);
J1 c= Polish-expression-hierarchy (L,E,(n + 1)) by A12, Th25;
then A22: rng (Polish-WFF-args F) c= J1 by A12, A14, Th71;
A30: for b being object st b in rng (Polish-WFF-args F) holds
H1 . b = H . b

proof

let b be object ; :: thesis: ( b in rng (Polish-WFF-args F) implies H1 . b = H . b )
assume A31: b in rng (Polish-WFF-args F) ; :: thesis: H1 . b = H . b
then consider m being Nat, J2 being Subset of (Polish-WFF-set (L,E)), H2 being Function of J2,D such that
A32: ( J2 = Polish-expression-hierarchy (L,E,m) & H2 is g -recursive ) and
A34: ( b in J2 & H . b = H2 . b ) by A1, A11;
thus H . b = H1 . b by A12, A13, A22, A31, A32, A34, Lm80; :: thesis: verum

end;

thus H . F = g . [(L -head F),(H1 * (Polish-WFF-args F))] by A13, A14, A15, A22
.= g . [(L -head F),(H * (Polish-WFF-args F))] by A11, A22, A30, Th72 ; :: thesis: verum