let P be FinSequence-membered set ; :: thesis: for A being Function of P,NAT
for U being Subset of (P *)
for u being FinSequence st u in Polish-expression-layer (P,A,U) holds
ex p, q being FinSequence st
( p in P & u = p ^ q )
let A be Function of P,NAT; :: thesis: for U being Subset of (P *)
for u being FinSequence st u in Polish-expression-layer (P,A,U) holds
ex p, q being FinSequence st
( p in P & u = p ^ q )
let U be Subset of (P *); :: thesis: for u being FinSequence st u in Polish-expression-layer (P,A,U) holds
ex p, q being FinSequence st
( p in P & u = p ^ q )
let u be FinSequence; :: thesis: ( u in Polish-expression-layer (P,A,U) implies ex p, q being FinSequence st
( p in P & u = p ^ q ) )
assume u in Polish-expression-layer (P,A,U) ; :: thesis: ex p, q being FinSequence st
( p in P & u = p ^ q )
then consider p, q being FinSequence, n being Nat such that
A1: ( u = p ^ q & p in P ) and
( n = A . p & q in U ^^ n ) by Def6;
thus ex p, q being FinSequence st
( p in P & u = p ^ q ) by A1; :: thesis: verum