theorem Th20: :: GROUP_1:21

for G being non empty unital multMagma holds 1_ G is_a_unity_wrt the multF of G