defpred S1[ object , object ] means for x1, y1, w1 being object st $1 = [x1,y1,w1] holds
P1[x1,y1,w1,$2];
A2:
for x being object st x in [:F1(),F2(),F3():] holds
ex z being object st
( z in F4() & S1[x,z] )
proof
let x be
object ;
( x in [:F1(),F2(),F3():] implies ex z being object st
( z in F4() & S1[x,z] ) )
assume
x in [:F1(),F2(),F3():]
;
ex z being object st
( z in F4() & S1[x,z] )
then consider x1,
y1,
w1 being
object such that A3:
(
x1 in F1() &
y1 in F2() &
w1 in F3() )
and A4:
x = [x1,y1,w1]
by MCART_1:68;
consider z being
object such that A5:
z in F4()
and A6:
P1[
x1,
y1,
w1,
z]
by A1, A3;
take
z
;
( z in F4() & S1[x,z] )
thus
z in F4()
by A5;
S1[x,z]
let x2,
y2,
w2 be
object ;
( x = [x2,y2,w2] implies P1[x2,y2,w2,z] )
assume A7a:
x = [x2,y2,w2]
;
P1[x2,y2,w2,z]
then
(
[x1,y1] = [x2,y2] &
w1 = w2 )
by A4, XTUPLE_0:1;
then
(
x1 = x2 &
y1 = y2 )
by XTUPLE_0:1;
hence
P1[
x2,
y2,
w2,
z]
by A6, A7a, A4, XTUPLE_0:1;
verum
end;
consider f being Function of [:F1(),F2(),F3():],F4() such that
A8:
for x being object st x in [:F1(),F2(),F3():] holds
S1[x,f . x]
from FUNCT_2:sch 1(A2);
take
f
; for x, y, w being object st x in F1() & y in F2() & w in F3() holds
P1[x,y,w,f . (x,y,w)]
thus
for x, y, w being object st x in F1() & y in F2() & w in F3() holds
P1[x,y,w,f . (x,y,w)]
by A8, MCART_1:69; verum