theorem Th4: :: MONOID_0:4

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