defpred S₁[ 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₁[f,g,z]

proof

let f, g be Element of product a; :: thesis: ex z being Element of product a st S₁[f,g,z]
defpred S₂[ set , set ] means ex i being Element of dom a st
( $1 = i & $2 = (b . i) . (f . i),(g . i) );
A2: for x being set st x in dom a holds
ex z being set st S₂[x,z]

proof

let x be set ; :: thesis: ( x in dom a implies ex z being set st S₂[x,z] )
assume x in dom a ; :: thesis: ex z being set st S₂[x,z]
then reconsider i = x as Element of dom a ;
take (b . i) . (f . i),(g . i) ; :: thesis: S₂[x,(b . i) . (f . i),(g . i)]
thus S₂[x,(b . i) . (f . i),(g . i)] ; :: thesis: verum

end;

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

now

let x be set ; :: 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;

then reconsider z9 = z as Element of product a by A3, CARD_3:18;
take z9 ; :: thesis: S₁[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;

consider d being BinOp of (product a) such that
A4: for f, g being Element of product a holds S₁[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