defpred S₁[ object , object ] means for x1, y1 being object st $1 = [x1,y1] holds
P₁[x1,y1,$2];
A3: for x, z being object st x in [:F₁(),F₂():] & S₁[x,z] holds
z in F₃()

proof

let x, z be object ; :: thesis: ( x in [:F₁(),F₂():] & S₁[x,z] implies z in F₃() )
assume x in [:F₁(),F₂():] ; :: thesis: ( not S₁[x,z] or z in F₃() )
then A4: ex x1, y1 being object st
( x1 in F₁() & y1 in F₂() & x = [x1,y1] ) by ZFMISC_1:def 2;
assume for x1, y1 being object st x = [x1,y1] holds
P₁[x1,y1,z] ; :: thesis: z in F₃()
hence z in F₃() by A1, A4; :: thesis: verum

end;

A5: for x, z1, z2 being object st x in [:F₁(),F₂():] & S₁[x,z1] & S₁[x,z2] holds
z1 = z2

proof

let x, z1, z2 be object ; :: thesis: ( x in [:F₁(),F₂():] & S₁[x,z1] & S₁[x,z2] implies z1 = z2 )
assume that
A6: x in [:F₁(),F₂():] and
A7: ( ( for x1, y1 being object st x = [x1,y1] holds
P₁[x1,y1,z1] ) & ( for x1, y1 being object st x = [x1,y1] holds
P₁[x1,y1,z2] ) ) ; :: thesis: z1 = z2
consider x1, y1 being object such that
A8: ( x1 in F₁() & y1 in F₂() ) and
A9: x = [x1,y1] by A6, ZFMISC_1:def 2;
( P₁[x1,y1,z1] & P₁[x1,y1,z2] ) by A7, A9;
hence z1 = z2 by A2, A8; :: thesis: verum

end;

consider f being PartFunc of [:F₁(),F₂():],F₃() such that
A10: for x being object holds
( x in dom f iff ( x in [:F₁(),F₂():] & ex z being object st S₁[x,z] ) ) and
A11: for x being object st x in dom f holds
S₁[x,f . x] from PARTFUN1:sch 2(A3, A5);
take f ; :: thesis: ( ( for x, y being object holds
( [x,y] in dom f iff ( x in F₁() & y in F₂() & ex z being object st P₁[x,y,z] ) ) ) & ( for x, y being object st [x,y] in dom f holds
P₁[x,y,f . (x,y)] ) )
thus for x, y being object holds
( [x,y] in dom f iff ( x in F₁() & y in F₂() & ex z being object st P₁[x,y,z] ) ) :: thesis: for x, y being object st [x,y] in dom f holds
P₁[x,y,f . (x,y)]

proof

let x, y be object ; :: thesis: ( [x,y] in dom f iff ( x in F₁() & y in F₂() & ex z being object st P₁[x,y,z] ) )
thus ( [x,y] in dom f implies ( x in F₁() & y in F₂() & ex z being object st P₁[x,y,z] ) ) :: thesis: ( x in F₁() & y in F₂() & ex z being object st P₁[x,y,z] implies [x,y] in dom f )

proof

assume A12: [x,y] in dom f ; :: thesis: ( x in F₁() & y in F₂() & ex z being object st P₁[x,y,z] )
hence ( x in F₁() & y in F₂() ) by ZFMISC_1:87; :: thesis: ex z being object st P₁[x,y,z]
consider z being object such that
A13: for x1, y1 being object st [x,y] = [x1,y1] holds
P₁[x1,y1,z] by A10, A12;
take z ; :: thesis: P₁[x,y,z]
thus P₁[x,y,z] by A13; :: thesis: verum

end;

assume ( x in F₁() & y in F₂() ) ; :: thesis: ( for z being object holds P₁[x,y,z] or [x,y] in dom f )
then A14: [x,y] in [:F₁(),F₂():] by ZFMISC_1:def 2;
given z being object such that A15: P₁[x,y,z] ; :: thesis: [x,y] in dom f

now :: thesis: ex z being object st
for x1, y1 being object st [x,y] = [x1,y1] holds
P₁[x1,y1,z]

take z = z; :: thesis: for x1, y1 being object st [x,y] = [x1,y1] holds
P₁[x1,y1,z]
let x1, y1 be object ; :: thesis: ( [x,y] = [x1,y1] implies P₁[x1,y1,z] )
assume A16: [x,y] = [x1,y1] ; :: thesis: P₁[x1,y1,z]
then x = x1 by XTUPLE_0:1;
hence P₁[x1,y1,z] by A15, A16, XTUPLE_0:1; :: thesis: verum

end;

hence [x,y] in dom f by A10, A14; :: thesis: verum

end;

thus for x, y being object st [x,y] in dom f holds
P₁[x,y,f . (x,y)] by A11; :: thesis: verum