:: deftheorem Def9 defines Polish-expression-hierarchy POLNOT_1:def 9 :
for P being FinSequence-membered set
for A being Function of P,NAT
for b₃ being Function holds
( b₃ = Polish-expression-hierarchy (P,A) iff ( dom b₃ = NAT & b₃ . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = b₃ . n & b₃ . (n + 1) = Polish-expression-layer (P,A,U) ) ) ) );