for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds 0. G is_a_unity_wrt the addF of G