:: deftheorem Def4 defines . MIDSP_2:def 4 :
for S being non empty set
for G being non empty addLoopStr
for w being Function of [:S,S:], the carrier of G
for a being Element of S
for x being Element of G st w is_atlas_of S,G holds
for b₆ being Element of S holds
( b₆ = (a,x) . w iff w . (a,b₆) = x );