Prime decomposition of knots

Every nontrivial oriented knot is a finite connected sum of knots of prime knots, uniquely up to permutation and oriented link isotopy. Existence follows by induction from additivity of Seifert genus. For uniqueness, compare complete decomposing sphere systems for a knot and remove their intersection circles by the prime-ball exchange lemma. Once a prime ball is disjoint from both systems, its factor can be removed from both; induction then matches all factors.