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 ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,n) & 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 n being Nat ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive )
let D be non empty set ; :: thesis: for g being Polish-recursion-function of E,D
for n being Nat ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive )
let g be Polish-recursion-function of E,D; :: thesis: for n being Nat ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive )
defpred S₁[ Nat] means ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,$1) & H is g -recursive );
A1: S₁[ 0 ] by Lm72;
A2: for n being Nat st S₁[n] holds
S₁[n + 1] by Lm75;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2); :: thesis: verum