:: deftheorem Def9 defines @ MIDSP_2:def 9 :
for S being non empty set
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for b₄ being BinOp of S holds
( b₄ = @ w iff for a, b being Element of S holds w . (a,(b₄ . (a,b))) = w . ((b₄ . (a,b)),b) );