consider Y being set such that
A2: for y being set holds
( y in Y iff ex x being set st
( x in F₁() & P₁[x,y] ) ) from TARSKI:sch 1(A1);
defpred S₁[ set ] means ex x, y being set st
( [x,y] = $1 & P₁[x,y] );
consider F being set such that
A3: for p being set holds
( p in F iff ( p in [:F₁(),Y:] & S₁[p] ) ) from XBOOLE_0:sch 1();

now

thus for p being set st p in F holds
ex x, y being set st [x,y] = p :: thesis: for x, y1, y2 being set st [x,y1] in F & [x,y2] in F holds
y1 = y2

proof

let p be set ; :: thesis: ( p in F implies ex x, y being set st [x,y] = p )
( p in F implies ex x, y being set st
( [x,y] = p & P₁[x,y] ) ) by A3;
hence ( p in F implies ex x, y being set st [x,y] = p ) ; :: thesis: verum

end;

let x, y1, y2 be set ; :: thesis: ( [x,y1] in F & [x,y2] in F implies y1 = y2 )
assume [x,y1] in F ; :: thesis: ( [x,y2] in F implies y1 = y2 )
then consider x1, z1 being set such that
A4: [x1,z1] = [x,y1] and
A5: P₁[x1,z1] by A3;
assume [x,y2] in F ; :: thesis: y1 = y2
then consider x2, z2 being set such that
A6: [x2,z2] = [x,y2] and
A7: P₁[x2,z2] by A3;
( x = x1 & z1 = y1 & x = x2 & z2 = y2 ) by A4, A6, ZFMISC_1:33;
hence y1 = y2 by A1, A5, A7; :: thesis: verum

end;

then reconsider f = F as Function by Def1, RELAT_1:def 1;
take f ; :: thesis: for x, y being set holds
( [x,y] in f iff ( x in F₁() & P₁[x,y] ) )
let x, y be set ; :: thesis: ( [x,y] in f iff ( x in F₁() & P₁[x,y] ) )
thus ( [x,y] in f implies ( x in F₁() & P₁[x,y] ) ) :: thesis: ( x in F₁() & P₁[x,y] implies [x,y] in f )

proof

assume A8: [x,y] in f ; :: thesis: ( x in F₁() & P₁[x,y] )
then [x,y] in [:F₁(),Y:] by A3;
hence x in F₁() by ZFMISC_1:106; :: thesis: P₁[x,y]
consider x1, y1 being set such that
A9: [x1,y1] = [x,y] and
A10: P₁[x1,y1] by A3, A8;
( x1 = x & y1 = y ) by A9, ZFMISC_1:33;
hence P₁[x,y] by A10; :: thesis: verum

end;

assume that
A11: x in F₁() and
A12: P₁[x,y] ; :: thesis: [x,y] in f
y in Y by A2, A11, A12;
then [x,y] in [:F₁(),Y:] by A11, ZFMISC_1:106;
hence [x,y] in f by A3, A12; :: thesis: verum