defpred S₁[ Element of X, Element of product F, Element of product F] means for i being Element of dom F holds $3 . i = (p . i) . ($1,($2 . i));
A1: for x being Element of X
for d being Element of product F ex z being Element of product F st S₁[x,d,z]

proof

let x be Element of X; :: thesis: for d being Element of product F ex z being Element of product F st S₁[x,d,z]
let d be Element of product F; :: thesis: ex z being Element of product F st S₁[x,d,z]
defpred S₂[ object , object ] means ex i being Element of dom F st
( $1 = i & $2 = (p . i) . (x,(d . i)) );
A2: for w being object st w in dom F holds
ex z being object st S₂[w,z]

proof

let w be object ; :: thesis: ( w in dom F implies ex z being object st S₂[w,z] )
assume w in dom F ; :: thesis: ex z being object st S₂[w,z]
then reconsider i = w as Element of dom F ;
take (p . i) . (x,(d . i)) ; :: thesis: S₂[w,(p . i) . (x,(d . i))]
thus S₂[w,(p . i) . (x,(d . i))] ; :: thesis: verum

end;

consider z being Function such that
A3: ( dom z = dom F & ( for w being object st w in dom F holds
S₂[w,z . w] ) ) from CLASSES1:sch 1(A2);

now :: thesis: for w being object st w in dom F holds
z . w in F . w

let w be object ; :: thesis: ( w in dom F implies z . w in F . w )
assume w in dom F ; :: thesis: z . w in F . w
then ex i being Element of dom F st
( w = i & z . w = (p . i) . (x,(d . i)) ) by A3;
hence z . w in F . w ; :: thesis: verum

end;

then reconsider z9 = z as Element of product F by A3, CARD_3:9;
take z9 ; :: thesis: S₁[x,d,z9]
let i be Element of dom F; :: thesis: z9 . i = (p . i) . (x,(d . i))
ex j being Element of dom F st
( j = i & z . i = (p . j) . (x,(d . j)) ) by A3;
hence z9 . i = (p . i) . (x,(d . i)) ; :: thesis: verum

end;

thus ex P being Function of [:X,(product F):],(product F) st
for x being Element of X
for d being Element of product F holds S₁[x,d,P . (x,d)] from BINOP_1:sch 3(A1); :: thesis: verum