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