theorem Th16: :: PRVECT_1:16

for a being Domain-Sequence
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