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

proof

let p be Element of [:F₁(),F₂(),F₃(),F₄():]; :: thesis: ex t being Element of F₅() st S₁[p,t]
consider x1, y1, z1, s1 being object such that
A3: x1 in F₁() and
A4: y1 in F₂() and
A5: z1 in F₃() and
A6: s1 in F₄() and
A7: p = [x1,y1,z1,s1] by MCART_1:79;
reconsider s1 = s1 as Element of F₄() by A6;
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
A8: P₁[x1,y1,z1,s1,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₃()
for s being Element of F₄() st p = [x,y,z,s] holds
P₁[x,y,z,s,t]
let y be Element of F₂(); :: thesis: for z being Element of F₃()
for s being Element of F₄() st p = [x,y,z,s] holds
P₁[x,y,z,s,t]
let z be Element of F₃(); :: thesis: for s being Element of F₄() st p = [x,y,z,s] holds
P₁[x,y,z,s,t]
let s be Element of F₄(); :: thesis: ( p = [x,y,z,s] implies P₁[x,y,z,s,t] )
assume A9: p = [x,y,z,s] ; :: thesis: P₁[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 P₁[x,y,z,s,t] by A7, A8, A9, A10, XTUPLE_0:5; :: thesis: verum

end;

consider f being Function of [:F₁(),F₂(),F₃(),F₄():],F₅() such that
A11: for p being Element of [:F₁(),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₃()
for s being Element of F₄() holds P₁[x,y,z,s,f . [x,y,z,s]]
let x be Element of F₁(); :: thesis: for y being Element of F₂()
for z being Element of F₃()
for s being Element of F₄() holds P₁[x,y,z,s,f . [x,y,z,s]]
let y be Element of F₂(); :: thesis: for z being Element of F₃()
for s being Element of F₄() holds P₁[x,y,z,s,f . [x,y,z,s]]
let z be Element of F₃(); :: thesis: for s being Element of F₄() holds P₁[x,y,z,s,f . [x,y,z,s]]
let s be Element of F₄(); :: thesis: P₁[x,y,z,s,f . [x,y,z,s]]
thus P₁[x,y,z,s,f . [x,y,z,s]] by A11; :: thesis: verum