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 t, q being FinSequence st
( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q & q in (Polish-expression-set (P,A)) ^^ n )
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 t, q being FinSequence st
( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q & q in (Polish-expression-set (P,A)) ^^ n )
let r be FinSequence; :: thesis: ( r in Polish-expression-set (P,A) implies ex n being Nat ex t, q being FinSequence st
( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q & q in (Polish-expression-set (P,A)) ^^ n ) )
assume r in Polish-expression-set (P,A) ; :: thesis: ex n being Nat ex t, q being FinSequence st
( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q & q in (Polish-expression-set (P,A)) ^^ n )
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 t, q being FinSequence, n being Nat such that
A4: r = t ^ q and
A5: t in P and
A6: n = A . t and
A7: q in (Polish-expression-hierarchy (P,A,m)) ^^ n by Def6;
take n ; :: thesis: ex t, q being FinSequence st
( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q & q in (Polish-expression-set (P,A)) ^^ n )
take t ; :: thesis: ex q being FinSequence st
( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q & q in (Polish-expression-set (P,A)) ^^ n )
take q ; :: thesis: ( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q & q in (Polish-expression-set (P,A)) ^^ n )
A10: (Polish-expression-hierarchy (P,A,m)) ^^ n c= (Polish-expression-set (P,A)) ^^ n by Th17, Th26;
then (Polish-expression-hierarchy (P,A,m)) ^^ n c= dom (Polish-operation (P,A,n,t)) by FUNCT_2:def 1;
hence ( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q & q in (Polish-expression-set (P,A)) ^^ n ) by A4, A5, A6, A7, A10, Def12; :: thesis: verum