theorem :: POLNOT_1:22

for P being FinSequence-membered set
for A being Function of P,NAT holds Polish-expression-hierarchy (P,A,0) = Polish-atoms (P,A) by Def9;