defpred S₂[ object , object ] means ex A being set st
( A = $2 & ( for y being object holds
( y in A iff ( y in F₂($1) & P₁[$1,y] ) ) ) );
A1: for x being object st x in F₁() holds
ex y being object st S₂[x,y]

proof

let x be object ; :: thesis: ( x in F₁() implies ex y being object st S₂[x,y] )
assume x in F₁() ; :: thesis: ex y being object st S₂[x,y]
defpred S₃[ object ] means P₁[x,$1];
consider Y being set such that
A2: for y being object holds
( y in Y iff ( y in F₂(x) & S₃[y] ) ) from XBOOLE_0:sch 1();
take Y ; :: thesis: S₂[x,Y]
reconsider A = Y as set ;
take A ; :: thesis: ( A = Y & ( for y being object holds
( y in A iff ( y in F₂(x) & P₁[x,y] ) ) ) )
thus ( A = Y & ( for y being object holds
( y in A iff ( y in F₂(x) & P₁[x,y] ) ) ) ) by A2; :: thesis: verum

end;

consider f being Function such that
A3: dom f = F₁() and
A4: for x being object st x in F₁() holds
S₂[x,f . x] from CLASSES1:sch 1(A1);
take f ; :: thesis: ( dom f = F₁() & ( for x being object st x in F₁() holds
for y being object holds
( y in f . x iff ( y in F₂(x) & P₁[x,y] ) ) ) )
thus dom f = F₁() by A3; :: thesis: for x being object st x in F₁() holds
for y being object holds
( y in f . x iff ( y in F₂(x) & P₁[x,y] ) )
let x be object ; :: thesis: ( x in F₁() implies for y being object holds
( y in f . x iff ( y in F₂(x) & P₁[x,y] ) ) )
assume x in F₁() ; :: thesis: for y being object holds
( y in f . x iff ( y in F₂(x) & P₁[x,y] ) )
then consider A being set such that
A5: A = f . x and
A6: for y being object holds
( y in A iff ( y in F₂(x) & P₁[x,y] ) ) by A4;
thus for y being object holds
( y in f . x iff ( y in F₂(x) & P₁[x,y] ) ) by A5, A6; :: thesis: verum