set X = bool (P *);
set Y = Polish-atoms (P,A);
reconsider Y = Polish-atoms (P,A) as Element of bool (P *) ;
defpred S₁[ set , set , set ] means ( $2 is Subset of (P *) implies ex V being Subset of (P *) st
( $2 = V & $3 = Polish-expression-layer (P,A,V) ) );
A2: for n being Nat
for U being Element of bool (P *) ex W being Element of bool (P *) st S₁[n,U,W]

let n be Nat; :: thesis:
let U be Element of bool (P *); :: thesis:
reconsider U = U as Subset of (P *) ;
set W = Polish-expression-layer (P,A,U);
reconsider W = Polish-expression-layer (P,A,U) as Element of bool (P *) ;
take W ; :: thesis:
thus S₁[n,U,W] ; :: thesis:

end;

consider f being sequence of (bool (P *)) such that
A14: f . 0 = Y and
A15: for n being Nat holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A2);
take f ; :: thesis:
defpred S₂[ Nat] means f . $1 is Subset of (P *);
A20: S₂[ 0 ] by A14;
A21: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis:
assume S₂[k] ; :: thesis:
then consider V being Subset of (P *) such that
f . k = V and
A24: f . (k + 1) = Polish-expression-layer (P,A,V) by A15;
thus S₂[k + 1] by A24; :: thesis:

end;

A26: for k being Nat holds S₂[k] from NAT_1:sch 2(A20, A21);
for n being Nat ex U being Subset of (P *) st
( U = f . n & f . (n + 1) = Polish-expression-layer (P,A,U) )

let n be Nat; :: thesis:
f . n is Subset of (P *) by A26;
then consider V being Subset of (P *) such that
A28: f . n = V and
A29: f . (n + 1) = Polish-expression-layer (P,A,V) by A15;
take V ; :: thesis:
thus ( V = f . n & f . (n + 1) = Polish-expression-layer (P,A,V) ) by A28, A29; :: thesis:

end;

hence ( dom f = NAT & f . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = f . n & f . (n + 1) = Polish-expression-layer (P,A,U) ) ) ) by A14, FUNCT_2:def 1; :: thesis: