:: deftheorem Def4 defines 1_ GROUP_1:def 4 :
for G being multMagma st G is unital holds
for b₂ being Element of G holds
( b₂ = 1_ G iff for h being Element of G holds
( h * b₂ = h & b₂ * h = h ) );