The proof has two parts: first show the operation $(aK)(bK) = abK$ is well-defined (independent of the choice of coset representatives), then verify the [group](/page/Group) axioms. **Step 1: Well-definedness of the operation.** [claim:Coset Multiplication Well Defined] If $aK = a'K$ and $bK = b'K$, then $abK = a'b'K$. [/claim] [proof] By the [Equal Cosets Criterion](/theorems/786), $a^{-1}a' = k_1 \in K$ and $b^{-1}b' = k_2 \in K$. We need $(ab)^{-1}(a'b') \in K$: \begin{align*} (ab)^{-1}(a'b') = b^{-1}a^{-1}a'b' = b^{-1}k_1 b' = b^{-1}k_1 (b \cdot b^{-1}b') = (b^{-1}k_1 b) k_2. \end{align*} Since $K \unlhd G$, we have $b^{-1}k_1 b \in K$ by the [Equivalent Definitions of Normality](/theorems/787). Call this $k_3 \in K$. Then $(ab)^{-1}(a'b') = k_3 k_2 \in K$ by closure. By the [Equal Cosets Criterion](/theorems/786), $abK = a'b'K$. [/proof] **Step 2: Group axioms.** - *Closure:* For $aK, bK \in G/K$, the product $abK \in G/K$ since $ab \in G$. - *Associativity:* $(aK)(bK \cdot cK) = (aK)(bcK) = a(bc)K = (ab)cK = (abK)(cK)$. - *Identity:* $K = eK$ satisfies $(aK)(eK) = aeK = aK = eaK = (eK)(aK)$. - *Inverses:* $(aK)(a^{-1}K) = aa^{-1}K = eK = K$, so $(aK)^{-1} = a^{-1}K$.