for G being non empty add-unital addMagma holds 0_ G is_a_unity_wrt the addF of G