A formal statement of the Fundamental Theorem of Arithmetic 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 $.

 A: 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. 
A: 
My problem is trying to define the 'product of a set'.

The rigorous way to define the product of a "set of numbers" usually goes something like this:
You know how to to define the product of two numbers, and you know the commutative law, so the order doesn't matter. Then the associative law tells you that you can write the product of three numbers in any order and with any arrangement of parentheses and always get the same answer. Then prove by induction that you can do the same for any finite set of numbers.
All along, be careful not to call these "sets" of numbers since sets can't have repeated elements. Call them "multisets" instead.
Once you've done all this you never have to think about it, and the usual formulation of the FToA stated seemingly informally is actually rigorous enough. You don't want to clutter up the statement with all this background stuff.
A: FToA can be written in first-order arithmetic using Gödel's $\beta$ function.
For every natural number $x$ we'll assert the existence of a natural number (actually two) coding a sequence in which the first element is $1$, every subsequent element is the product of the previous element and a (non-decreasing) prime, and the last element is $x$.  To define this we'll have to look at triples of consecutive elements of the sequence.
The statement starts off looking like this:
$\exists_{a,b} (\beta(a,b,0)=1 \land \exists_j(\beta(a,b,j)=x \land 
\forall_i (i \lt j \rightarrow \exists_q(\text{Prime}(q) \land \beta(a,b,i) \cdot q = \beta(a,b,i+1) \land \dots$
So far this asserts that the first element is $1$ and the ratios of consecutive elements of the sequence are prime.  What I omitted is that the ratios must be non-decreasing.
Finally as you suggest we can assert this sequence is unique.  If $P(a,b,x)$ represents everything under $\exists_{a,b}$ above, then we can write something like:
$\forall_x (x \lt 2 \vee \forall_{a,b,c,d}(P(a,b,x) \land P(c,d,x) \rightarrow \forall_i{(\beta(a,b,i) = \beta(c,d,i))})$
