let d, d' be BinOp of product a; :: 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) ) & ( 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) ) implies d = d' )
assume that
A6: 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) and
A7: 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) ; :: thesis: d = d'

now

let f, g be Element of product a; :: thesis: for i being Element of dom a holds (d . f,g) . i = (d' . f,g) . i
let i be Element of dom a; :: thesis: (d . f,g) . i = (d' . f,g) . i
thus (d . f,g) . i = (b . i) . (f . i),(g . i) by A6
.= (d' . f,g) . i by A7 ; :: thesis: verum

end;

hence d = d' by Th24; :: thesis: verum