theorem Th21: :: GROUP_1:22

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