set X = bool (P *);
set Y = Polish-atoms (P,A);
reconsider Y = Polish-atoms (P,A) as Element of bool (P *) ;
defpred S1[ 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 S1[n,U,W]
proof
let n be
Nat;
for U being Element of bool (P *) ex W being Element of bool (P *) st S1[n,U,W]let U be
Element of
bool (P *);
ex W being Element of bool (P *) st S1[n,U,W]
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
;
S1[n,U,W]
thus
S1[
n,
U,
W]
;
verum
end;
consider f being sequence of (bool (P *)) such that
A14:
f . 0 = Y
and
A15:
for n being Nat holds S1[n,f . n,f . (n + 1)]
from RECDEF_1:sch 2(A2);
take
f
; ( 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) ) ) )
defpred S2[ Nat] means f . $1 is Subset of (P *);
A20:
S2[ 0 ]
by A14;
A21:
for k being Nat st S2[k] holds
S2[k + 1]
A26:
for k being Nat holds S2[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) )
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; verum