for X being set
for G being non empty unital multMagma holds 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G)