theorem Th23: :: POLNOT_1:23

for P being FinSequence-membered set
for A being Function of P,NAT
for n being Nat holds Polish-expression-hierarchy (P,A,(n + 1)) = Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,n)))