for M being MidSp
for a, b, c being Element of M holds a @ (b @ c) = (a @ b) @ (a @ c)