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
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J 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 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 & J c= J1 & H1 is g -recursive & a in J 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 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 & J c= J1 & H1 is g -recursive & a in J 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 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 & J c= J1 & H1 is g -recursive & a in J 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 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 & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
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
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
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
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J 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 & J c= J1 & H1 is g -recursive & a in J 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 & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
let a be object ; :: thesis: ( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J implies H . a = H1 . a )
assume that
A1: J = Polish-expression-hierarchy (L,E,n) and
A2: H is g -recursive and
A3: J c= J1 and
A4: H1 is g -recursive and
A5: a in J ; :: thesis: H . a = H1 . a
defpred S₁[ Nat] means for a being object st a in J & a in Polish-expression-hierarchy (L,E,$1) holds
H . a = H1 . a;
A10: S₁[ 0 ]

proof

let a be object ; :: thesis: ( a in J & a in Polish-expression-hierarchy (L,E,0) implies H . a = H1 . a )
assume A11: a in J ; :: thesis: ( not a in Polish-expression-hierarchy (L,E,0) or H . a = H1 . a )
then reconsider G = a as Polish-WFF of L,E ;
assume a in Polish-expression-hierarchy (L,E,0) ; :: thesis: H . a = H1 . a
then A13: a in Polish-atoms (L,E) by Def9;
then a in L by Def7;
then Polish-WFF-head G = G by Th53;
then Polish-arity G = 0 by A13, Def7;
then A15: Polish-WFF-args G = {} by Th61;
then A16: rng (Polish-WFF-args G) c= J ;
A17: rng (Polish-WFF-args G) c= J1 by A15;
thus H . a = g . [(L -head G),(H * {})] by A2, A11, A15, A16
.= g . [(L -head G),(H1 * {})]
.= H1 . a by A3, A4, A11, A15, A17 ; :: thesis: verum

end;

A20: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A21: S₁[k] ; :: thesis: S₁[k + 1]
set J2 = Polish-expression-hierarchy (L,E,k);
set J3 = Polish-expression-hierarchy (L,E,(k + 1));
let a be object ; :: thesis: ( a in J & a in Polish-expression-hierarchy (L,E,(k + 1)) implies H . a = H1 . a )
assume A22: a in J ; :: thesis: ( not a in Polish-expression-hierarchy (L,E,(k + 1)) or H . a = H1 . a )
assume A23: a in Polish-expression-hierarchy (L,E,(k + 1)) ; :: thesis: H . a = H1 . a

per cases ( n <= k or k < n ) ;

suppose n <= k ; :: thesis: H . a = H1 . a

then consider m being Nat such that
A24: k = n + m by NAT_1:10;
J c= Polish-expression-hierarchy (L,E,k) by A1, A24, Th25;
then reconsider G = a as Element of Polish-expression-hierarchy (L,E,k) by A22;
thus H . a = H1 . G by A21, A22
.= H1 . a ; :: thesis: verum

end;

suppose k < n ; :: thesis: H . a = H1 . a

then k + 1 <= n by NAT_1:13;
then consider m being Nat such that
A30: n = (k + 1) + m by NAT_1:10;
A31: Polish-expression-hierarchy (L,E,(k + 1)) c= J by A1, A30, Th25;
reconsider F1 = a as Polish-WFF of L,E by A22;
A32: rng (Polish-WFF-args F1) c= Polish-expression-hierarchy (L,E,k) by A23, Th71;
Polish-expression-hierarchy (L,E,k) c= Polish-expression-hierarchy (L,E,(k + 1)) by Th25;
then A33: rng (Polish-WFF-args F1) c= J by A31, A32;
then A34: rng (Polish-WFF-args F1) c= J1 by A3;
for b being object st b in rng (Polish-WFF-args F1) holds
H . b = H1 . b by A21, A32, A33;
then A37: H * (Polish-WFF-args F1) = H1 * (Polish-WFF-args F1) by A33, A34, Th72;
thus H . a = g . [(L -head F1),(H * (Polish-WFF-args F1))] by A2, A22, A33
.= H1 . a by A3, A4, A22, A34, A37 ; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A20);
hence H . a = H1 . a by A1, A5; :: thesis: verum