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
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D st J = Polish-expression-hierarchy (L,E,n) & J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H 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))] ) holds
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
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D st J = Polish-expression-hierarchy (L,E,n) & J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H 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))] ) holds
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
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D st J = Polish-expression-hierarchy (L,E,n) & J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H 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))] ) holds
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
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D st J = Polish-expression-hierarchy (L,E,n) & J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H 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))] ) holds
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
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D st J = Polish-expression-hierarchy (L,E,n) & J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H 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))] ) holds
H1 is g -recursive
let J be Subset of (Polish-WFF-set (L,E)); :: thesis: for H being Function of J,D
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D st J = Polish-expression-hierarchy (L,E,n) & J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H 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))] ) holds
H1 is g -recursive
let H be Function of J,D; :: thesis: for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D st J = Polish-expression-hierarchy (L,E,n) & J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H 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))] ) holds
H1 is g -recursive
let J1 be Subset of (Polish-WFF-set (L,E)); :: thesis: for H1 being Function of J1,D st J = Polish-expression-hierarchy (L,E,n) & J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H 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))] ) holds
H1 is g -recursive
let H1 be Function of J1,D; :: thesis: ( J = Polish-expression-hierarchy (L,E,n) & J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H 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))] ) implies H1 is g -recursive )
assume that
A1: J = Polish-expression-hierarchy (L,E,n) and
A2: J1 = Polish-expression-hierarchy (L,E,(n + 1)) and
A3: H is g -recursive and
A4: for F being Polish-WFF of L,E st F in J1 holds
H1 . F = g . [(L -head F),(H * (Polish-WFF-args F))] ; :: thesis: H1 is g -recursive
A5: J c= J1 by A1, A2, Th25;
A6: for a being object st a in J holds
H1 . a = H . a

proof

let a be object ; :: thesis: ( a in J implies H1 . a = H . a )
assume A10: a in J ; :: thesis: H1 . a = H . a
reconsider G1 = a as Polish-WFF of L,E by A10;
reconsider F = a as Element of J by A10;
A12: rng (Polish-WFF-args G1) c= J by A1, A2, A5, A10, Th71;
thus H1 . a = g . [(L -head F),(H * (Polish-WFF-args G1))] by A4, A5, A10
.= H . a by A3, A10, A12 ; :: thesis: verum

end;

let F be Polish-WFF of L,E; :: according to POLNOT_1:def 43 :: thesis: ( F in J1 & rng (Polish-WFF-args F) c= J1 implies H1 . F = g . [(L -head F),(H1 * (Polish-WFF-args F))] )
assume that
A20: F in J1 and
A21: rng (Polish-WFF-args F) c= J1 ; :: thesis: H1 . F = g . [(L -head F),(H1 * (Polish-WFF-args F))]
A23: rng (Polish-WFF-args F) c= J by A1, A2, A20, Th71;
then A24: for a being object st a in rng (Polish-WFF-args F) holds
H . a = H1 . a by A6;
A27: H * (Polish-WFF-args F) = H1 * (Polish-WFF-args F) by A21, A23, A24, Th72;
thus H1 . F = g . [(L -head F),(H1 * (Polish-WFF-args F))] by A4, A20, A27; :: thesis: verum