Smooth and topological knot concordance classes form abelian groups

In the smooth category, [F1] makes the smooth concordance classes a quotient set. [F2] ensures that replacing either connected-sum input by a concordant knot leaves the resulting class unchanged, so connected sum defines a binary operation on that quotient. [F3] supplies associativity, commutativity, and the two-sided identity on oriented knot types; these equalities pass to the quotient because the operation is well-defined.

For every $K$, [F4] gives a smooth disk bounded by $K\mathrm{\#}{K}^{†}$. By [F5], this connected sum is smoothly concordant to the standard unknot, so $[K]+[K^{†}]=[U]$ in the smooth quotient. Together with the commutative monoid structure from step 1.1, every element has an inverse; thus the smooth quotient is an abelian group with the stated inverse.

In the locally flat topological category, [F1] again gives a quotient set, and the TOP implication of [F2] makes connected sum independent of both concordance representatives. Associativity, commutativity and the unknot identity descend from [F3] exactly as in step 1.1. For each smooth knot representative $K$, the smooth disk from [F4] and its smooth concordance to $U$ from [F5] are also locally flat by the surface/collar convention. Therefore $[K]+[K^{†}]=[U]$ in the TOP quotient. Every element has the stated inverse, so this quotient too is an abelian group. The Countable Choice strength here is that of the bounded compatibility specialization [F2], not an unstated full-AC hypothesis.