for O being set
for G being GroupWithOperators of O holds nat_hom ((1). G) is bijective