let P be FinSequence-membered set ; :: thesis: 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)))
let A be Function of P,NAT; :: thesis: for n being Nat holds Polish-expression-hierarchy (P,A,(n + 1)) = Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,n)))
let n be Nat; :: thesis: Polish-expression-hierarchy (P,A,(n + 1)) = Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,n)))
consider U being Subset of (P *) such that
A1: U = Polish-expression-hierarchy (P,A,n) and
A2: Polish-expression-hierarchy (P,A,(n + 1)) = Polish-expression-layer (P,A,U) by Def9;
thus Polish-expression-hierarchy (P,A,(n + 1)) = Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,n))) by A1, A2; :: thesis: verum