Suppose and . Since , the second equality also gives , so and for some . Thus for some , and the operation is well-defined.

Associativity follows from associativity in . The identity is , the inverse of is , and closure follows from the definition of the operation. Hence is a group.