theorem Th25: :: POLNOT_1:25

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