theorem :: GROUP_7:31

for G1 being non empty Group-like multMagma holds 1_ (product <*G1*>) = <*(1_ G1)*>