let G be non empty add-unital addMagma ; :: thesis: the_unity_wrt the addF of G = 0_ G
0_ G is_a_unity_wrt the addF of G by Th20;
hence the_unity_wrt the addF of G = 0_ G by BINOP_1:def 8; :: thesis: verum