defpred S₁[ object ] means ( $1 in P * & ex p, q being FinSequence ex n being Nat st
( $1 = p ^ q & p in P & n = A . p & q in U ^^ n ) );
consider Y being set such that
A1: for a being object holds
( a in Y iff ( a in P * & S₁[a] ) ) from XBOOLE_0:sch 1();
Y c= P * by A1;
then reconsider Y = Y as Subset of (P *) ;
take Y ; :: thesis: for a being object holds
( a in Y iff ( a in P * & ex p, q being FinSequence ex n being Nat st
( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) )
thus for a being object holds
( a in Y iff ( a in P * & ex p, q being FinSequence ex n being Nat st
( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) ) by A1; :: thesis: verum