:: deftheorem Def2 defines * TOPGRP_1:def 2 :
for G being non empty multMagma
for a being Element of G
for b₃ being Function of G,G holds
( b₃ = * a iff for x being Element of G holds b₃ . x = x * a );