let P be FinSequence-membered set ; :: thesis: for A being Function of P,NAT
for r being FinSequence st r in Polish-expression-set (P,A) holds
ex n being Nat ex p, q being FinSequence st
( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n & r = p ^ q )
let A be Function of P,NAT; :: thesis: for r being FinSequence st r in Polish-expression-set (P,A) holds
ex n being Nat ex p, q being FinSequence st
( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n & r = p ^ q )
let r be FinSequence; :: thesis: ( r in Polish-expression-set (P,A) implies ex n being Nat ex p, q being FinSequence st
( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n & r = p ^ q ) )
assume r in Polish-expression-set (P,A) ; :: thesis: ex n being Nat ex p, q being FinSequence st
( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n & r = p ^ q )
then consider m being Nat such that
A1: r in Polish-expression-hierarchy (P,A,(m + 1)) by Th28;
set U = Polish-expression-hierarchy (P,A,m);
r in Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,m))) by A1, Th23;
then consider p, q being FinSequence, n being Nat such that
A2: r = p ^ q and
A3: p in P and
A4: n = A . p and
A5: q in (Polish-expression-hierarchy (P,A,m)) ^^ n by Def6;
take n ; :: thesis: ex p, q being FinSequence st
( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n & r = p ^ q )
take p ; :: thesis: ex q being FinSequence st
( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n & r = p ^ q )
take q ; :: thesis: ( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n & r = p ^ q )
(Polish-expression-hierarchy (P,A,m)) ^^ n c= (Polish-expression-set (P,A)) ^^ n by Th26, Th17;
hence ( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n & r = p ^ q ) by A2, A3, A4, A5; :: thesis: verum