defpred S_{1}[ 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_{1}[x,d,z]

for x being Element of X

for d being Element of product F holds S_{1}[x,d,P . (x,d)]
from BINOP_1:sch 3(A1); :: thesis: verum

A1: for x being Element of X

for d being Element of product F ex z being Element of product F st S

proof

thus
ex P being Function of [:X,(product F):],(product F) st
let x be Element of X; :: thesis: for d being Element of product F ex z being Element of product F st S_{1}[x,d,z]

let d be Element of product F; :: thesis: ex z being Element of product F st S_{1}[x,d,z]

defpred S_{2}[ 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_{2}[w,z]

A3: ( dom z = dom F & ( for w being object st w in dom F holds

S_{2}[w,z . w] ) )
from CLASSES1:sch 1(A2);

take z9 ; :: thesis: S_{1}[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;let d be Element of product F; :: thesis: ex z being Element of product F st S

defpred S

( $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

proof

consider z being Function such that
let w be object ; :: thesis: ( w in dom F implies ex z being object st S_{2}[w,z] )

assume w in dom F ; :: thesis: ex z being object st S_{2}[w,z]

then reconsider i = w as Element of dom F ;

take (p . i) . (x,(d . i)) ; :: thesis: S_{2}[w,(p . i) . (x,(d . i))]

thus S_{2}[w,(p . i) . (x,(d . i))]
; :: thesis: verum

end;assume w in dom F ; :: thesis: ex z being object st S

then reconsider i = w as Element of dom F ;

take (p . i) . (x,(d . i)) ; :: thesis: S

thus S

A3: ( dom z = dom F & ( for w being object st w in dom F holds

S

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

z . w in F . w

then reconsider z9 = z as Element of product F by A3, CARD_3:9;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;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

take z9 ; :: thesis: S

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

for x being Element of X

for d being Element of product F holds S