defpred S₁[ object , object ] means P₁[$1,$2 `1 ,$2 `2 ];
A2: for e being Element of F₁() ex u being Element of [:F₂(),F₃():] st S₁[e,u]

proof

let e be Element of F₁(); :: thesis: ex u being Element of [:F₂(),F₃():] st S₁[e,u]
consider ai being Element of F₂(), bi being Element of F₃() such that
A3: P₁[e,ai,bi] by A1;
reconsider u = [ai,bi] as Element of [:F₂(),F₃():] by ZFMISC_1:87;
take u ; :: thesis: S₁[e,u]
thus S₁[e,u] by A3; :: thesis: verum

end;

consider f being Function of F₁(),[:F₂(),F₃():] such that
A4: for e being Element of F₁() holds S₁[e,f . e] from FUNCT_2:sch 3(A2);
take pr1 f ; :: thesis: ex b being Function of F₁(),F₃() st
for i being Element of F₁() holds P₁[i,(pr1 f) . i,b . i]
take pr2 f ; :: thesis: for i being Element of F₁() holds P₁[i,(pr1 f) . i,(pr2 f) . i]
let i be Element of F₁(); :: thesis: P₁[i,(pr1 f) . i,(pr2 f) . i]
A5: (f . i) `2 = (pr2 f) . i by FUNCT_2:def 6;
(f . i) `1 = (pr1 f) . i by FUNCT_2:def 5;
hence P₁[i,(pr1 f) . i,(pr2 f) . i] by A4, A5; :: thesis: verum