consider D being non empty set such that
A0: P c= D * by FINSEQ_1:85;
set E = bool (D *);
reconsider E = bool (D *) as non empty set ;
set W = {(<*> D)};
{(<*> D)} c= D *

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {(<*> D)} or a in D * )
assume a in {(<*> D)} ; :: thesis: a in D *
then a = <*> D by TARSKI:def 1;
hence a in D * by FINSEQ_1:def 11; :: thesis: verum

end;

then reconsider W = {(<*> D)} as Element of E ;
defpred S₁[ set , set , set ] means ex Q being FinSequence-membered set st
( $2 = Q & $3 = Q ^ P );
A2: for n being Nat
for Q being Element of E ex R being Element of E st S₁[n,Q,R]

proof

let n be Nat; :: thesis: for Q being Element of E ex R being Element of E st S₁[n,Q,R]
let Q be Element of E; :: thesis: ex R being Element of E st S₁[n,Q,R]
reconsider Q = Q as FinSequence-membered set ;
set R = Q ^ P;
Q ^ P c= D *

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Q ^ P or a in D * )
assume a in Q ^ P ; :: thesis: a in D *
then consider p, q being FinSequence such that
A3: ( a = p ^ q & p in Q & q in P ) by Def2;
reconsider p = p as FinSequence of D by FINSEQ_1:def 11, A3;
reconsider q = q as FinSequence of D by FINSEQ_1:def 11, A3, A0;
p ^ q is FinSequence of D ;
then reconsider a = a as FinSequence of D by A3;
a in D * by FINSEQ_1:def 11;
hence a in D * ; :: thesis: verum

end;

then reconsider R = Q ^ P as Element of E ;
take R ; :: thesis: S₁[n,Q,R]
thus S₁[n,Q,R] ; :: thesis: verum

end;

consider f being sequence of E such that
A14: f . 0 = W and
A15: for n being Nat holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A2);
take f ; :: thesis: ( dom f = NAT & f . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = f . n & f . (n + 1) = Q ^ P ) ) )
thus ( dom f = NAT & f . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = f . n & f . (n + 1) = Q ^ P ) ) ) by A14, A15, FUNCT_2:def 1; :: thesis: verum