theorem Th18: :: PRVECT_1:18

for a being Domain-Sequence
for b being BinOps of a st ( for i being Element of dom a holds b . i is associative ) holds
[:b:] is associative