:: deftheorem Def1 defines * TOPGRP_1:def 1 :
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 = a * x );