Definition of a group with redundancy?

[Syrus]

Homework Statement

I would define a group as follows:

A group consists of a non-empty set G together with a binary operation (say, *) on G such that the following axioms hold:

G1...G2...G3...

Homework Equations

The Attempt at a Solution

I know this is a trivial question, but doesn't a binary operation on a set (here G) necesserily imply that the set is closed under that binary operation? The only reason i ask is that many of the definitions of groups I have come across include both that * is a binary operation under which G is closed. Isn't this redundant?

 

[micromass]

It all depends on how you define a binary operation. I would define it as a function

$$*:G\times G\rightarrow G$$

If you define a binary operation like that, then the property you mention is indeed redundant.

I guess, that many authors include that property because most readers aren't yet ready to view a binary operation as a function. So to make it easy on them, they include the axiom that G is closed.