defpred S_{1}[ Element of product a, Element of product a, Element of product a] means for i being Element of dom a holds $3 . i = (b . i) . (($1 . i),($2 . i));

A1: for f, g being Element of product a ex z being Element of product a st S_{1}[f,g,z]

A4: for f, g being Element of product a holds S_{1}[f,g,d . (f,g)]
from BINOP_1:sch 3(A1);

take d ; :: thesis: for f, g being Element of product a

for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i))

thus for f, g being Element of product a

for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i)) by A4; :: thesis: verum

A1: for f, g being Element of product a ex z being Element of product a st S

proof

consider d being BinOp of (product a) such that
let f, g be Element of product a; :: thesis: ex z being Element of product a st S_{1}[f,g,z]

defpred S_{2}[ object , object ] means ex i being Element of dom a st

( $1 = i & $2 = (b . i) . ((f . i),(g . i)) );

A2: for x being object st x in dom a holds

ex z being object st S_{2}[x,z]

A3: ( dom z = dom a & ( for x being object st x in dom a holds

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

take z9 ; :: thesis: S_{1}[f,g,z9]

let i be Element of dom a; :: thesis: z9 . i = (b . i) . ((f . i),(g . i))

ex j being Element of dom a st

( j = i & z . i = (b . j) . ((f . j),(g . j)) ) by A3;

hence z9 . i = (b . i) . ((f . i),(g . i)) ; :: thesis: verum

end;defpred S

( $1 = i & $2 = (b . i) . ((f . i),(g . i)) );

A2: for x being object st x in dom a holds

ex z being object st S

proof

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

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

then reconsider i = x as Element of dom a ;

take (b . i) . ((f . i),(g . i)) ; :: thesis: S_{2}[x,(b . i) . ((f . i),(g . i))]

thus S_{2}[x,(b . i) . ((f . i),(g . i))]
; :: thesis: verum

end;assume x in dom a ; :: thesis: ex z being object st S

then reconsider i = x as Element of dom a ;

take (b . i) . ((f . i),(g . i)) ; :: thesis: S

thus S

A3: ( dom z = dom a & ( for x being object st x in dom a holds

S

now :: thesis: for x being object st x in dom a holds

z . x in a . x

then reconsider z9 = z as Element of product a by A3, CARD_3:9;z . x in a . x

let x be object ; :: thesis: ( x in dom a implies z . x in a . x )

assume x in dom a ; :: thesis: z . x in a . x

then ex i being Element of dom a st

( x = i & z . x = (b . i) . ((f . i),(g . i)) ) by A3;

hence z . x in a . x ; :: thesis: verum

end;assume x in dom a ; :: thesis: z . x in a . x

then ex i being Element of dom a st

( x = i & z . x = (b . i) . ((f . i),(g . i)) ) by A3;

hence z . x in a . x ; :: thesis: verum

take z9 ; :: thesis: S

let i be Element of dom a; :: thesis: z9 . i = (b . i) . ((f . i),(g . i))

ex j being Element of dom a st

( j = i & z . i = (b . j) . ((f . j),(g . j)) ) by A3;

hence z9 . i = (b . i) . ((f . i),(g . i)) ; :: thesis: verum

A4: for f, g being Element of product a holds S

take d ; :: thesis: for f, g being Element of product a

for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i))

thus for f, g being Element of product a

for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i)) by A4; :: thesis: verum