defpred S₁[ set , set ] means for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃() st $1 = [x,y,z] holds
P₁[x,y,z,$2];
A2: for p being Element of [:F₁(),F₂(),F₃():] ex t being Element of F₄() st S₁[p,t]

proof

let p be Element of [:F₁(),F₂(),F₃():]; :: thesis: ex t being Element of F₄() st S₁[p,t]
consider x1, y1, z1 being set such that
A3: x1 in F₁() and
A4: y1 in F₂() and
A5: z1 in F₃() and
A6: p = [x1,y1,z1] by MCART_1:72;
reconsider z1 = z1 as Element of F₃() by A5;
reconsider y1 = y1 as Element of F₂() by A4;
reconsider x1 = x1 as Element of F₁() by A3;
consider t being Element of F₄() such that
A7: P₁[x1,y1,z1,t] by A1;
take t ; :: thesis: S₁[p,t]
let x be Element of F₁(); :: thesis: for y being Element of F₂()
for z being Element of F₃() st p = [x,y,z] holds
P₁[x,y,z,t]
let y be Element of F₂(); :: thesis: for z being Element of F₃() st p = [x,y,z] holds
P₁[x,y,z,t]
let z be Element of F₃(); :: thesis: ( p = [x,y,z] implies P₁[x,y,z,t] )
assume A8: p = [x,y,z] ; :: thesis: P₁[x,y,z,t]
then ( x1 = x & y1 = y ) by A6, MCART_1:28;
hence P₁[x,y,z,t] by A6, A7, A8, MCART_1:28; :: thesis: verum

end;

consider f being Function of [:F₁(),F₂(),F₃():],F₄() such that
A9: for p being Element of [:F₁(),F₂(),F₃():] holds S₁[p,f . p] from FUNCT_2:sch 3(A2);
take f ; :: thesis: for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃() holds P₁[x,y,z,f . [x,y,z]]
let x be Element of F₁(); :: thesis: for y being Element of F₂()
for z being Element of F₃() holds P₁[x,y,z,f . [x,y,z]]
let y be Element of F₂(); :: thesis: for z being Element of F₃() holds P₁[x,y,z,f . [x,y,z]]
let z be Element of F₃(); :: thesis: P₁[x,y,z,f . [x,y,z]]
thus P₁[x,y,z,f . [x,y,z]] by A9; :: thesis: verum