let d, d9 be BinOp of (product a); ( ( 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 (d9 . (f,g)) . i = (b . i) . ((f . i),(g . i)) ) implies d = d9 )
assume that
A5:
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
A6:
for f, g being Element of product a
for i being Element of dom a holds (d9 . (f,g)) . i = (b . i) . ((f . i),(g . i))
; d = d9
hence
d = d9
by Th16; verum