theorem :: GROUP_4:9

for G being non empty multMagma
for a being Element of G holds Product <*a*> = a by FINSOP_1:11;