The Product of Cosets of a Normal Subgroup Is Well Defined and Makes the Cosets a Group

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $(G,\cdot)$ be a group, with identity element $e$ and the inverse $g^{-1}$ of each $g\in G$, unique by Uniqueness of the Identity Element and of Inverses in a Group (i) and Uniqueness of the Identity Element and of Inverses in a Group (ii). Let $N$ be a normal subgroup of $G$, let $gN$ be the left coset of $N$ determined by $g\in G$, and let $G/N$ be the set of left cosets of $N$.

(i) Products of cosets. There is exactly one binary operation $\ast$ on $G/N$ such that

$$(gN)\ast(hN)=(g\cdot h)N\qquad\text{for all } g,h\in G.$$

(ii) The cosets form a group. The pair $(G/N,\ast)$, with $\ast$ the operation of (i), is a group. Its identity element is $N=eN$, and the inverse of $gN$ is $g^{-1}N$ for every $g\in G$.

(iii) The projection. The function $g\mapsto gN$ from $G$ to $G/N$ is a surjective group homomorphism from $(G,\cdot)$ to $(G/N,\ast)$, and its kernel is $N$.