defpred S_{1}[ object , object ] means P_{1}[$1,$2 `1 ,$2 `2 ];

A2: for e being Element of F_{1}() ex u being Element of [:F_{2}(),F_{3}():] st S_{1}[e,u]
_{1}(),[:F_{2}(),F_{3}():] such that

A4: for e being Element of F_{1}() holds S_{1}[e,f . e]
from FUNCT_2:sch 3(A2);

take pr1 f ; :: thesis: ex b being Function of F_{1}(),F_{3}() st

for i being Element of F_{1}() holds P_{1}[i,(pr1 f) . i,b . i]

take pr2 f ; :: thesis: for i being Element of F_{1}() holds P_{1}[i,(pr1 f) . i,(pr2 f) . i]

let i be Element of F_{1}(); :: thesis: P_{1}[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_{1}[i,(pr1 f) . i,(pr2 f) . i]
by A4, A5; :: thesis: verum

A2: for e being Element of F

proof

consider f being Function of F
let e be Element of F_{1}(); :: thesis: ex u being Element of [:F_{2}(),F_{3}():] st S_{1}[e,u]

consider ai being Element of F_{2}(), bi being Element of F_{3}() such that

A3: P_{1}[e,ai,bi]
by A1;

reconsider u = [ai,bi] as Element of [:F_{2}(),F_{3}():] by ZFMISC_1:87;

take u ; :: thesis: S_{1}[e,u]

thus S_{1}[e,u]
by A3; :: thesis: verum

end;consider ai being Element of F

A3: P

reconsider u = [ai,bi] as Element of [:F

take u ; :: thesis: S

thus S

A4: for e being Element of F

take pr1 f ; :: thesis: ex b being Function of F

for i being Element of F

take pr2 f ; :: thesis: for i being Element of F

let i be Element of F

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