and then the injective character follows from the action being free. There is a fourth property that follows from 1, 2 above:
#

Existence of one-to-one translations

#: For all , the mapping is a bijection.

Property 3 is often used in the following equivalent form (the 5th property).
#

Subtraction:

#: For every in , there exists a unique , denoted , such that .Another way to express