theorem :: MONOID_1:56

for G being non empty unital multMagma holds 1. (bool G) = {(the_unity_wrt the multF of G)}