defpred S1[ set , set ] means for x being Element of F1()
for y being Element of F2() st \$1 = [x,y] holds
P1[x,y,\$2];
A2: for p being Element of [:F1(),F2():] ex z being Element of F3() st S1[p,z]
proof
let p be Element of [:F1(),F2():]; :: thesis: ex z being Element of F3() st S1[p,z]
consider x1, y1 being object such that
A3: x1 in F1() and
A4: y1 in F2() and
A5: p = [x1,y1] by ZFMISC_1:def 2;
reconsider y1 = y1 as Element of F2() by A4;
reconsider x1 = x1 as Element of F1() by A3;
consider z being Element of F3() such that
A6: P1[x1,y1,z] by A1;
take z ; :: thesis: S1[p,z]
let x be Element of F1(); :: thesis: for y being Element of F2() st p = [x,y] holds
P1[x,y,z]

let y be Element of F2(); :: thesis: ( p = [x,y] implies P1[x,y,z] )
assume A7: p = [x,y] ; :: thesis: P1[x,y,z]
then x1 = x by ;
hence P1[x,y,z] by A5, A6, A7, XTUPLE_0:1; :: thesis: verum
end;
consider f being Function of [:F1(),F2():],F3() such that
A8: for p being Element of [:F1(),F2():] holds S1[p,f . p] from take f ; :: thesis: for x being Element of F1()
for y being Element of F2() holds P1[x,y,f . (x,y)]

let x be Element of F1(); :: thesis: for y being Element of F2() holds P1[x,y,f . (x,y)]
let y be Element of F2(); :: thesis: P1[x,y,f . (x,y)]
reconsider xy = [x,y] as Element of [:F1(),F2():] by ZFMISC_1:def 2;
P1[x,y,f . xy] by A8;
hence P1[x,y,f . (x,y)] ; :: thesis: verum