defpred S₁[ set , set ] means ( $1 in F₁() & P₁[$1,$2] );
A3: for x, y1, y2 being set st S₁[x,y1] & S₁[x,y2] holds
y1 = y2 by A1;
consider f being Function such that
A4: for x, y being set holds
( [x,y] in f iff ( x in F₁() & S₁[x,y] ) ) from FUNCT_1:sch 1(A3);
take f ; :: thesis: ( dom f = F₁() & ( for x being set st x in F₁() holds
P₁[x,f . x] ) )
for x being set holds
( x in dom f iff x in F₁() )

proof

let x be set ; :: thesis: ( x in dom f iff x in F₁() )
thus ( x in dom f implies x in F₁() ) :: thesis: ( x in F₁() implies x in dom f )

proof

assume x in dom f ; :: thesis: x in F₁()
then ex y being set st [x,y] in f by RELAT_1:def 4;
hence x in F₁() by A4; :: thesis: verum

end;

assume A5: x in F₁() ; :: thesis: x in dom f
then consider y being set such that
A6: P₁[x,y] by A2;
[x,y] in f by A4, A5, A6;
hence x in dom f by RELAT_1:def 4; :: thesis: verum

end;

hence A7: dom f = F₁() by TARSKI:1; :: thesis: for x being set st x in F₁() holds
P₁[x,f . x]
let x be set ; :: thesis: ( x in F₁() implies P₁[x,f . x] )
assume A8: x in F₁() ; :: thesis: P₁[x,f . x]
then consider y being set such that
A9: P₁[x,y] by A2;
[x,y] in f by A4, A8, A9;
hence P₁[x,f . x] by A7, A8, A9, Def4; :: thesis: verum