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 )
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 )
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 ) )
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 )
then consider m being Nat such that
A1: r in Polish-expression-hierarchy (P,A,(m + 1)) by Th37;
set U = Polish-expression-hierarchy (P,A,m);
r in Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,m))) by A1, Th31;
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 Def8;
take n ; :: thesis: ex t, q being FinSequence st
( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q )
take t ; :: thesis: ex q being FinSequence st
( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q )
take q ; :: thesis: ( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q )
dom (Polish-operation (P,A,n,t)) = (Polish-expression-set (P,A)) ^^ n by FUNCT_2:def 1;
then (Polish-expression-hierarchy (P,A,m)) ^^ n c= dom (Polish-operation (P,A,n,t)) by Th35, TH18;
hence ( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q ) by A4, A5, A6, A7, Def13; :: thesis: verum