let G be non empty multMagma ; :: thesis: ( G is unital implies the_unity_wrt the multF of G is_a_unity_wrt the multF of G )
given a being Element of G such that A1: a is_a_unity_wrt H₂(G) ; :: according to SETWISEO:def 2,MONOID_0:def 10 :: thesis: the_unity_wrt the multF of G is_a_unity_wrt the multF of G
thus the_unity_wrt the multF of G is_a_unity_wrt the multF of G by A1, BINOP_1:def 8; :: thesis: verum