defpred S₁[ object , object ] means for x1, y1, w1 being object st $1 = [x1,y1,w1] holds
P₁[x1,y1,w1,$2];
A2: for x being object st x in [:F₁(),F₂(),F₃():] holds
ex z being object st
( z in F₄() & S₁[x,z] )

proof

let x be object ; :: thesis: ( x in [:F₁(),F₂(),F₃():] implies ex z being object st
( z in F₄() & S₁[x,z] ) )
assume x in [:F₁(),F₂(),F₃():] ; :: thesis: ex z being object st
( z in F₄() & S₁[x,z] )
then consider x1, y1, w1 being object such that
A3: ( x1 in F₁() & y1 in F₂() & w1 in F₃() ) and
A4: x = [x1,y1,w1] by MCART_1:68;
consider z being object such that
A5: z in F₄() and
A6: P₁[x1,y1,w1,z] by A1, A3;
take z ; :: thesis: ( z in F₄() & S₁[x,z] )
thus z in F₄() by A5; :: thesis: S₁[x,z]
let x2, y2, w2 be object ; :: thesis: ( x = [x2,y2,w2] implies P₁[x2,y2,w2,z] )
assume A7a: x = [x2,y2,w2] ; :: thesis: P₁[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 P₁[x2,y2,w2,z] by A6, A7a, A4, XTUPLE_0:1; :: thesis: verum

end;

consider f being Function of [:F₁(),F₂(),F₃():],F₄() such that
A8: for x being object st x in [:F₁(),F₂(),F₃():] holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
take f ; :: thesis: for x, y, w being object st x in F₁() & y in F₂() & w in F₃() holds
P₁[x,y,w,f . (x,y,w)]
thus for x, y, w being object st x in F₁() & y in F₂() & w in F₃() holds
P₁[x,y,w,f . (x,y,w)] by A8, MCART_1:69; :: thesis: verum