let a be Domain-Sequence; :: thesis: for d, d9 being BinOp of (product a) st ( for f, g being Element of product a
for i being Element of dom a holds (d . f,g) . i = (d9 . f,g) . i ) holds
d = d9
let d, d9 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 = (d9 . f,g) . i ) implies d = d9 )
assume A1: for f, g being Element of product a
for i being Element of dom a holds (d . f,g) . i = (d9 . f,g) . i ; :: thesis: d = d9

now

let f, g be Element of product a; :: thesis: d . f,g = d9 . f,g
A2: ( dom (d . f,g) = dom a & dom (d9 . f,g) = dom a ) by CARD_3:18;
for x being set st x in dom a holds
(d . f,g) . x = (d9 . f,g) . x by A1;
hence d . f,g = d9 . f,g by A2, FUNCT_1:9; :: thesis: verum

end;

hence d = d9 by BINOP_1:2; :: thesis: verum