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