defpred S1[ 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 S1[f,g,z]
proof
let f, g be Element of product a; :: thesis: ex z being Element of product a st S1[f,g,z]
defpred S2[ 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 S2[x,z]
proof
let x be object ; :: thesis: ( x in dom a implies ex z being object st S2[x,z] )
assume x in dom a ; :: thesis: ex z being object st S2[x,z]
then reconsider i = x as Element of dom a ;
take (b . i) . ((f . i),(g . i)) ; :: thesis: S2[x,(b . i) . ((f . i),(g . i))]
thus S2[x,(b . i) . ((f . i),(g . i))] ; :: thesis: verum
end;
consider z being Function such that
A3: ( dom z = dom a & ( for x being object st x in dom a holds
S2[x,z . x] ) ) from
now :: thesis: for x being object st x in dom a holds
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;
then reconsider z9 = z as Element of product a by ;
take z9 ; :: thesis: S1[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 () such that
A4: for f, g being Element of product a holds S1[f,g,d . (f,g)] from 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