The point of my post was to point that there are things that are not OK with the way we usually define Groups.

I’m a real formalist and for me logical correctness matters just like it matters if a proof depends on the axiom of Choice or not and just as it matters that a sequence is a function from the set of natural numbers.

But I’m also trying to learn how to be a real Software Engineer and thus for me usability also matters. Definitions should be what is used, not the consequences of them (as is the case with the usual definition for Group).