for G being non empty multMagma st G is unital holds
the_unity_wrt the multF of G is_a_unity_wrt the multF of G