defpred S1[ object , object ] means P1[\$1,\$2 `1 ,\$2 `2 ];
A2: for e being Element of F1() ex u being Element of [:F2(),F3():] st S1[e,u]
proof
let e be Element of F1(); :: thesis: ex u being Element of [:F2(),F3():] st S1[e,u]
consider ai being Element of F2(), bi being Element of F3() such that
A3: P1[e,ai,bi] by A1;
reconsider u = [ai,bi] as Element of [:F2(),F3():] by ZFMISC_1:87;
take u ; :: thesis: S1[e,u]
thus S1[e,u] by A3; :: thesis: verum
end;
consider f being Function of F1(),[:F2(),F3():] such that
A4: for e being Element of F1() holds S1[e,f . e] from take pr1 f ; :: thesis: ex b being Function of F1(),F3() st
for i being Element of F1() holds P1[i,(pr1 f) . i,b . i]

take pr2 f ; :: thesis: for i being Element of F1() holds P1[i,(pr1 f) . i,(pr2 f) . i]
let i be Element of F1(); :: thesis: P1[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 P1[i,(pr1 f) . i,(pr2 f) . i] by A4, A5; :: thesis: verum