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