defpred S₁[ object , object ] means ( $1 in F₁() & P₁[$1,$2] );
A3: for x, y1, y2 being object st S₁[x,y1] & S₁[x,y2] holds
y1 = y2 by A1;
consider f being Function such that
A4: for x, y being object 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 object st x in F₁() holds
P₁[x,f . x] ) )
for x being object holds
( x in dom f iff x in F₁() )

proof

let x be object ; :: 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 object st [x,y] in f by XTUPLE_0:def 12;
hence x in F₁() by A4; :: thesis: verum

end;

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

end;

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