let G be non empty unital multMagma ; :: thesis: the_unity_wrt the multF of G = 1_ G
1_ G is_a_unity_wrt the multF of G by Th20;
hence the_unity_wrt the multF of G = 1_ G by BINOP_1:def 8; :: thesis: verum