defpred S₂[ set ] means ex p being FinSequence st
( P₁[p] & $1 = p );
consider Y being set such that
A1: for x being set holds
( x in Y iff ( x in F₁() * & S₂[x] ) ) from XBOOLE_0:sch 1();
take Y ; :: thesis: for x being set holds
( x in Y iff ex p being FinSequence st
( p in F₁() * & P₁[p] & x = p ) )
for x being set holds
( x in Y iff ex p being FinSequence st
( p in F₁() * & P₁[p] & x = p ) )

proof

let x be set ; :: thesis: ( x in Y iff ex p being FinSequence st
( p in F₁() * & P₁[p] & x = p ) )

now

assume x in Y ; :: thesis: ex p being FinSequence st
( p in F₁() * & P₁[p] & x = p )
then ( x in F₁() * & ex p being FinSequence st
( P₁[p] & x = p ) ) by A1;
hence ex p being FinSequence st
( p in F₁() * & P₁[p] & x = p ) ; :: thesis: verum

end;

hence ( x in Y iff ex p being FinSequence st
( p in F₁() * & P₁[p] & x = p ) ) by A1; :: thesis: verum

end;

hence for x being set holds
( x in Y iff ex p being FinSequence st
( p in F₁() * & P₁[p] & x = p ) ) ; :: thesis: verum