defpred S1[ object , object ] means for x1, y1 being object st \$1 = [x1,y1] holds
P1[x1,y1,\$2];
A2: for x being object st x in [:F1(),F2():] holds
ex z being object st
( z in F3() & S1[x,z] )
proof
let x be object ; :: thesis: ( x in [:F1(),F2():] implies ex z being object st
( z in F3() & S1[x,z] ) )

assume x in [:F1(),F2():] ; :: thesis: ex z being object st
( z in F3() & S1[x,z] )

then consider x1, y1 being object such that
A3: ( x1 in F1() & y1 in F2() ) and
A4: x = [x1,y1] by ZFMISC_1:def 2;
consider z being object such that
A5: z in F3() and
A6: P1[x1,y1,z] by A1, A3;
take z ; :: thesis: ( z in F3() & S1[x,z] )
thus z in F3() by A5; :: thesis: S1[x,z]
let x2, y2 be object ; :: thesis: ( x = [x2,y2] implies P1[x2,y2,z] )
assume A7: x = [x2,y2] ; :: thesis: P1[x2,y2,z]
then x1 = x2 by ;
hence P1[x2,y2,z] by A4, A6, A7, XTUPLE_0:1; :: thesis: verum
end;
consider f being Function of [:F1(),F2():],F3() such that
A8: for x being object st x in [:F1(),F2():] holds
S1[x,f . x] from take f ; :: thesis: for x, y being object st x in F1() & y in F2() holds
P1[x,y,f . (x,y)]

let x, y be object ; :: thesis: ( x in F1() & y in F2() implies P1[x,y,f . (x,y)] )
assume ( x in F1() & y in F2() ) ; :: thesis: P1[x,y,f . (x,y)]
then [x,y] in [:F1(),F2():] by ZFMISC_1:def 2;
hence P1[x,y,f . (x,y)] by A8; :: thesis: verum