defpred S₁[ set , set ] 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;
take [ai,bi] ; :: thesis: ( [ai,bi] is Element of [:F₂(),F₃():] & S₁[e,[ai,bi]] )
thus [ai,bi] is Element of [:F₂(),F₃():] by ZFMISC_1:106; :: thesis: S₁[e,[ai,bi]]
[ai,bi] `1 = ai by MCART_1:7;
hence S₁[e,[ai,bi]] by A3, MCART_1:7; :: 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 7;
(f . i) `1 = (pr1 f) . i by FUNCT_2:def 6;
hence P₁[i,(pr1 f) . i,(pr2 f) . i] by A4, A5; :: thesis: verum