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():];
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
;
S1[p,z]
let x be
Element of
F1();
for y being Element of F2() st p = [x,y] holds
P1[x,y,z]let y be
Element of
F2();
( p = [x,y] implies P1[x,y,z] )
assume A7:
p = [x,y]
;
P1[x,y,z]
then
x1 = x
by A5, XTUPLE_0:1;
hence
P1[
x,
y,
z]
by A5, A6, A7, XTUPLE_0:1;
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 FUNCT_2:sch 3(A2);
take
f
; 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(); for y being Element of F2() holds P1[x,y,f . (x,y)]
let y be Element of F2(); 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)]
; verum