let P be FinSequence-membered set ; 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; 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 *); 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; ( 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)
; 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 Def8;
thus
ex p, q being FinSequence st
( p in P & u = p ^ q )
by A1; verum