:: deftheorem Def2 defines -con_map WEDDWITT:def 2 :
for G being Group
for a being Element of G
for b₃ being Function of the carrier of G,(con_class a) holds
( b₃ = a -con_map iff for x being Element of G holds b₃ . x = a |^ x );