How can we formalize the Fundamental Theorem of Arithmetic in such a way as to make it more rigorous (i.e.using sets, etc.)?
My attempt
We say that a set of prime numbers $A $ "defines" a natural number $ n $ if the 'product of the elements of this set' is equal to $ n $". My problem is trying to define the 'product of a set'. In this way, we can reformulate the Fundamental Theorem of Arithmetic as the statement
If $A $ and $B $ defines a natural number $ n $ then $ A = B $.
If you want something fancy: Consider $\mathbb N$ (with $0$) and the set $S=\mathbb N^\mathbb N$, the set of functions $f\colon \mathbb N \to \mathbb N$. Let $S_0=\{f\in S\mid f(n)=0 \quad \mathrm{almost \quad always}\}$. Let $P_0,P_1,\dots$ be an enumeration of the primes with no repetition. FToA: The function $g\colon S_0\to \mathbb N$ given by $g(f)=\Pi_{n\in \mathbb N} P_n^{f(n)}$ is bijective. In more detail, surjectivity states that every natural number is the product of primes, and injectivity states the product is unique in the appropriate sense.