:: deftheorem Def8 defines Polish-expression-layer POLNOT_1:def 6 :
for P being FinSequence-membered set
for A being Function of P,NAT
for U, b₄ being Subset of (P *) holds
( b₄ = Polish-expression-layer (P,A,U) iff for a being object holds
( a in b₄ iff ( a in P * & ex p, q being FinSequence ex n being Nat st
( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) ) );