defpred S1[ set , set ] means for x being Element of F1()
for y being Element of F2()
for z being Element of F3() st $1 = [x,y,z] holds
P1[x,y,z,$2];
A2:
for p being Element of [:F1(),F2(),F3():] ex t being Element of F4() st S1[p,t]
proof
let p be
Element of
[:F1(),F2(),F3():];
ex t being Element of F4() st S1[p,t]
consider x1,
y1,
z1 being
object such that A3:
x1 in F1()
and A4:
y1 in F2()
and A5:
z1 in F3()
and A6:
p = [x1,y1,z1]
by MCART_1:68;
reconsider z1 =
z1 as
Element of
F3()
by A5;
reconsider y1 =
y1 as
Element of
F2()
by A4;
reconsider x1 =
x1 as
Element of
F1()
by A3;
consider t being
Element of
F4()
such that A7:
P1[
x1,
y1,
z1,
t]
by A1;
take
t
;
S1[p,t]
let x be
Element of
F1();
for y being Element of F2()
for z being Element of F3() st p = [x,y,z] holds
P1[x,y,z,t]let y be
Element of
F2();
for z being Element of F3() st p = [x,y,z] holds
P1[x,y,z,t]let z be
Element of
F3();
( p = [x,y,z] implies P1[x,y,z,t] )
assume A8:
p = [x,y,z]
;
P1[x,y,z,t]
then
(
x1 = x &
y1 = y )
by A6, XTUPLE_0:3;
hence
P1[
x,
y,
z,
t]
by A6, A7, A8, XTUPLE_0:3;
verum
end;
consider f being Function of [:F1(),F2(),F3():],F4() such that
A9:
for p being Element of [:F1(),F2(),F3():] 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()
for z being Element of F3() holds P1[x,y,z,f . [x,y,z]]
let x be Element of F1(); for y being Element of F2()
for z being Element of F3() holds P1[x,y,z,f . [x,y,z]]
let y be Element of F2(); for z being Element of F3() holds P1[x,y,z,f . [x,y,z]]
let z be Element of F3(); P1[x,y,z,f . [x,y,z]]
thus
P1[x,y,z,f . [x,y,z]]
by A9; verum