defpred S₁[ object , object ] means for x, y being object st $1 = [x,y] holds
P₁[x,y,$2];
set D = [:F₁(),F₂():];
A3: for p being object st p in [:F₁(),F₂():] holds
ex z being object st S₁[p,z]

proof

let p be object ; :: thesis: ( p in [:F₁(),F₂():] implies ex z being object st S₁[p,z] )
assume p in [:F₁(),F₂():] ; :: thesis: ex z being object st S₁[p,z]
then consider x1, y1 being object such that
A4: ( x1 in F₁() & y1 in F₂() ) and
A5: p = [x1,y1] by ZFMISC_1:def 2;
consider z being object such that
A6: P₁[x1,y1,z] by A2, A4;
take z ; :: thesis: S₁[p,z]
let x, y be object ; :: thesis: ( p = [x,y] implies P₁[x,y,z] )
assume A7: p = [x,y] ; :: thesis: P₁[x,y,z]
then x = x1 by A5, XTUPLE_0:1;
hence P₁[x,y,z] by A5, A6, A7, XTUPLE_0:1; :: thesis: verum

end;

A8: for p, y1, y2 being object st p in [:F₁(),F₂():] & S₁[p,y1] & S₁[p,y2] holds
y1 = y2

proof

let p, y1, y2 be object ; :: thesis: ( p in [:F₁(),F₂():] & S₁[p,y1] & S₁[p,y2] implies y1 = y2 )
assume p in [:F₁(),F₂():] ; :: thesis: ( not S₁[p,y1] or not S₁[p,y2] or y1 = y2 )
then consider x1, x2 being object such that
A9: ( x1 in F₁() & x2 in F₂() ) and
A10: p = [x1,x2] by ZFMISC_1:def 2;
assume ( ( for x, y being object st p = [x,y] holds
P₁[x,y,y1] ) & ( for x, y being object st p = [x,y] holds
P₁[x,y,y2] ) ) ; :: thesis: y1 = y2
then ( P₁[x1,x2,y1] & P₁[x1,x2,y2] ) by A10;
hence y1 = y2 by A1, A9; :: thesis: verum

end;

consider f being Function such that
A11: dom f = [:F₁(),F₂():] and
A12: for p being object st p in [:F₁(),F₂():] holds
S₁[p,f . p] from FUNCT_1:sch 2(A8, A3);
take f ; :: thesis: ( dom f = [:F₁(),F₂():] & ( for x, y being object st x in F₁() & y in F₂() holds
P₁[x,y,f . (x,y)] ) )
thus dom f = [:F₁(),F₂():] by A11; :: thesis: for x, y being object st x in F₁() & y in F₂() holds
P₁[x,y,f . (x,y)]
let x, y be object ; :: thesis: ( x in F₁() & y in F₂() implies P₁[x,y,f . (x,y)] )
assume ( x in F₁() & y in F₂() ) ; :: thesis: P₁[x,y,f . (x,y)]
then [x,y] in [:F₁(),F₂():] by ZFMISC_1:def 2;
hence P₁[x,y,f . (x,y)] by A12; :: thesis: verum