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

proof

let x be object ; :: thesis:

now :: thesis:

assume x in Y ; :: thesis:
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:

end;

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

end;

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