let P be FinSequence-membered set ; :: thesis: for A being Function of P,NAT holds Polish-expression-set (P,A) is A -closed
let A be Function of P,NAT; :: thesis: Polish-expression-set (P,A) is A -closed
let p be FinSequence; :: according to POLNOT_1:def 15 :: thesis: for n being Nat
for q being FinSequence st p in dom A & n = A . p & q in (Polish-expression-set (P,A)) ^^ n holds
p ^ q in Polish-expression-set (P,A)
let n be Nat; :: thesis: for q being FinSequence st p in dom A & n = A . p & q in (Polish-expression-set (P,A)) ^^ n holds
p ^ q in Polish-expression-set (P,A)
let q be FinSequence; :: thesis: ( p in dom A & n = A . p & q in (Polish-expression-set (P,A)) ^^ n implies p ^ q in Polish-expression-set (P,A) )
assume that
A1: p in dom A and
A2: n = A . p and
A3: q in (Polish-expression-set (P,A)) ^^ n ; :: thesis: p ^ q in Polish-expression-set (P,A)
consider m being Nat such that
A4: q in (Polish-expression-hierarchy (P,A,m)) ^^ n by A3, Th27;
set U = Polish-expression-hierarchy (P,A,m);
dom A = P by FUNCT_2:def 1;
then p ^ q in Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,m))) by A1, A2, A4, Th18;
then p ^ q in Polish-expression-hierarchy (P,A,(m + 1)) by Th23;
hence p ^ q in Polish-expression-set (P,A) by Th26, TARSKI:def 3; :: thesis: verum