defpred S1[ object , object ] means for x1, y1 being object st $1 = [x1,y1] holds
P1[x1,y1,$2];
A3: for x, z being object st x in [:F1(),F2():] & S1[x,z] holds
z in F3()
proof
let x, z be object ; :: thesis: ( x in [:F1(),F2():] & S1[x,z] implies z in F3() )
assume x in [:F1(),F2():] ; :: thesis: ( not S1[x,z] or z in F3() )
then A4: ex x1, y1 being object st
( x1 in F1() & y1 in F2() & x = [x1,y1] ) by ZFMISC_1:def 2;
assume for x1, y1 being object st x = [x1,y1] holds
P1[x1,y1,z] ; :: thesis: z in F3()
hence z in F3() by A1, A4; :: thesis: verum
end;
A5: for x, z1, z2 being object st x in [:F1(),F2():] & S1[x,z1] & S1[x,z2] holds
z1 = z2
proof
let x, z1, z2 be object ; :: thesis: ( x in [:F1(),F2():] & S1[x,z1] & S1[x,z2] implies z1 = z2 )
assume that
A6: x in [:F1(),F2():] and
A7: ( ( for x1, y1 being object st x = [x1,y1] holds
P1[x1,y1,z1] ) & ( for x1, y1 being object st x = [x1,y1] holds
P1[x1,y1,z2] ) ) ; :: thesis: z1 = z2
consider x1, y1 being object such that
A8: ( x1 in F1() & y1 in F2() ) and
A9: x = [x1,y1] by A6, ZFMISC_1:def 2;
( P1[x1,y1,z1] & P1[x1,y1,z2] ) by A7, A9;
hence z1 = z2 by A2, A8; :: thesis: verum
end;
consider f being PartFunc of [:F1(),F2():],F3() such that
A10: for x being object holds
( x in dom f iff ( x in [:F1(),F2():] & ex z being object st S1[x,z] ) ) and
A11: for x being object st x in dom f holds
S1[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 F1() & y in F2() & ex z being object st P1[x,y,z] ) ) ) & ( for x, y being object st [x,y] in dom f holds
P1[x,y,f . (x,y)] ) )
thus for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being object st P1[x,y,z] ) ) :: thesis: for x, y being object st [x,y] in dom f holds
P1[x,y,f . (x,y)]
proof
let x, y be object ; :: thesis: ( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being object st P1[x,y,z] ) )
thus ( [x,y] in dom f implies ( x in F1() & y in F2() & ex z being object st P1[x,y,z] ) ) :: thesis: ( x in F1() & y in F2() & ex z being object st P1[x,y,z] implies [x,y] in dom f )
proof
assume A12: [x,y] in dom f ; :: thesis: ( x in F1() & y in F2() & ex z being object st P1[x,y,z] )
hence ( x in F1() & y in F2() ) by ZFMISC_1:87; :: thesis: ex z being object st P1[x,y,z]
consider z being object such that
A13: for x1, y1 being object st [x,y] = [x1,y1] holds
P1[x1,y1,z] by A10, A12;
take z ; :: thesis: P1[x,y,z]
thus P1[x,y,z] by A13; :: thesis: verum
end;
assume ( x in F1() & y in F2() ) ; :: thesis: ( for z being object holds P1[x,y,z] or [x,y] in dom f )
then A14: [x,y] in [:F1(),F2():] by ZFMISC_1:def 2;
given z being object such that A15: P1[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
P1[x1,y1,z]
take z = z; :: thesis: for x1, y1 being object st [x,y] = [x1,y1] holds
P1[x1,y1,z]
let x1, y1 be object ; :: thesis: ( [x,y] = [x1,y1] implies P1[x1,y1,z] )
assume A16: [x,y] = [x1,y1] ; :: thesis: P1[x1,y1,z]
then x = x1 by XTUPLE_0:1;
hence P1[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
P1[x,y,f . (x,y)] by A11; :: thesis: verum