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

now :: thesis: ( ( for p being object st p in F holds
ex x, y being object st [x,y] = p ) & ( for x, y1, y2 being object st [x,y1] in F & [x,y2] in F holds
y1 = y2 ) )

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

proof

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

end;

let x, y1, y2 be object ; :: 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 object such that
A4: [x1,z1] = [x,y1] and
A5: P₁[x1,z1] by A3;
A6: ( x = x1 & z1 = y1 ) by A4, XTUPLE_0:1;
assume [x,y2] in F ; :: thesis: y1 = y2
then consider x2, z2 being object such that
A7: [x2,z2] = [x,y2] and
A8: P₁[x2,z2] by A3;
( x = x2 & z2 = y2 ) by A7, XTUPLE_0:1;
hence y1 = y2 by A1, A5, A8, A6; :: thesis: verum

end;

then reconsider f = F as Function by Def1, RELAT_1:def 1;
take f ; :: thesis: for x, y being object holds
( [x,y] in f iff ( x in F₁() & P₁[x,y] ) )
let x, y be object ; :: 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 A9: [x,y] in f ; :: thesis: ( x in F₁() & P₁[x,y] )
then consider x1, y1 being object such that
A10: [x1,y1] = [x,y] and
A11: P₁[x1,y1] by A3;
[x,y] in [:F₁(),Y:] by A3, A9;
hence x in F₁() by ZFMISC_1:87; :: thesis: P₁[x,y]
x1 = x by A10, XTUPLE_0:1;
hence P₁[x,y] by A10, A11, XTUPLE_0:1; :: thesis: verum

end;

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