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
for a, b1, b2, c being Point of M st w is_atlas_of the carrier of M,G & w is associating holds
( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )