theorem Th19: :: MIDSP_2:19

for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for M being non empty MidStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
for a, b, c, d being Point of M holds (a @ b) @ (c @ d) = (a @ c) @ (b @ d)