for S being non empty set
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for a, b, b9, c, c9 being Element of S st w . (a,b) = w . (b,c) & w . (a,b9) = w . (b9,c9) holds
w . (c,c9) = Double (w . (b,b9))