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 m being Nat
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 holds
H . a = H1 . 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 n being Nat
for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D
for m being Nat
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 holds
H . a = H1 . a
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 m being Nat
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 holds
H . a = H1 . a
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 m being Nat
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 holds
H . a = H1 . a
let n be Nat; :: thesis: for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D
for m being Nat
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 holds
H . a = H1 . a
let J be Subset of (Polish-WFF-set (L,E)); :: thesis: for H being Function of J,D
for m being Nat
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 holds
H . a = H1 . a
let H be Function of J,D; :: thesis: for m being Nat
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 holds
H . a = H1 . a
let m be Nat; :: thesis: for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 holds
H . a = H1 . a
let J1 be Subset of (Polish-WFF-set (L,E)); :: thesis: for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 holds
H . a = H1 . a
let H1 be Function of J1,D; :: thesis: for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 holds
H . a = H1 . a
let a be object ; :: thesis: ( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 implies H . a = H1 . a )
assume that
A1: J = Polish-expression-hierarchy (L,E,n) and
A2: H is g -recursive and
A3: J1 = Polish-expression-hierarchy (L,E,m) and
A4: H1 is g -recursive and
A5: a in J and
A6: a in J1 ; :: thesis: H . a = H1 . a
consider J2 being Subset of (Polish-WFF-set (L,E)), H2 being Function of J2,D such that
A10: J2 = Polish-expression-hierarchy (L,E,(n + m)) and
A11: H2 is g -recursive by Th74;
thus H . a = H2 . a by A1, A2, A5, A10, A11, Th25, Lm74
.= H1 . a by A3, A4, A6, A10, A11, Th25, Lm74 ; :: thesis: verum