Unique characterization of tensor product state by map on fully separable states Some article on quantum mechanics that I'm currently reading contains an unproved claim that I don't understand. I will explain it further below.
Let $H_1$ and $H_2$ be Hilbert spaces, and let $S_1$ and $S_2$ denote the corresponding state spaces, so $S_i$ is the set of all onedimensional subspaces of $H_i$ for each $i$. With $S_1 \otimes S_2$ we denote the set of all states in the tensor product. Furthermore we call such a state $s$ of $S_1 \otimes S_2$ separable if $s = s_1 \otimes s_2$ for some $s_1 \in S_1$ and $s_2 \in S_2$. The set of separable states is hence simply $S_1 \times S_2$.
Then the following holds:
Any quantum state $s$ in $S_1 \otimes S_2$ is (up to multiplicative scalar) uniquely characterized by the function mapping any separable state $x = x_1 \otimes x_2 \in S_1 \times S_2$ to the probability $| \langle s , x \rangle |^2$ of $s$ collapsing to $x$ (after a measurement in a basis that includes $x$).
Given such an $s$ in $S_1 \otimes S_2$, we can indeed consider an associated map 
$ F_s : S_1 \times S_2 \rightarrow [0,1]$ defined by $ x  \mapsto | \langle s , x \rangle |^2$ (where $ x= x_1 \otimes x_2$ with $x_1 \in S_1$ and $x_2 \in S_2$). However, why does the uniqueness hold? That I don't see.
First of all: what does it even mean here, that this is a "unique characterization"?
I think that it means the following: for all $s, t \in S_1 \otimes S_2$, if it holds that $F_s (x) = F_{t} (x)$ for all $x \in S_1 \times S_2$, then $s=t$. I am, however, unsure about this.
Concretely my two questions are:


*

*Is my above interpretation of the "unique characterization" correct?

*How does one prove the above statement?
(Note: by picking a basis $\{b_1 , \ldots , b_n \}$ of $S_1 \otimes S_2$ and then writing $s$ and $t$ with respect to that basis, it is easy to see that, for each $i$, $\langle b_i , s \rangle$ and $\langle b_i , s \rangle$ are equal up to a phase factor. However this phase factor seems to depend on $i$, and for that reason I could not finish the proof.)
 A: First, consider a single Hilbert space $\mathcal H_1$. (All Hilbert spaces are assumed to be finite-dimensional.)  Then, the set of all $\{\lvert s\rangle\langle s\rvert\}$ is an overcomplete basis for the set of all matrices. (For hermitian matrices, this follows from the eigendecomposition, and every matrix $M$ is of the form $M=A+iB$ with $A$, $B$ hermitian.)
Now consider product states $\lvert s_1\rangle \otimes \lvert s_2\rangle$, $s_1\in\mathcal H_1$, $s_2\in\mathcal H_2$.  The corresponding projectors $\lvert s_1\rangle\langle s_1\rvert \otimes \lvert s_2\rangle\langle s_2\rvert$ form an overcomplete basis for all matrices: First, every matrix $M$ can be written as $M=\sum A_i\otimes B_i$, and second, each $A_i$ and $B_i$ can be expressed in terms of $\lvert s_{\bullet}\rangle\langle s_{\bullet}\rvert$, as we have seen above.
This means that we can select a basis $\lvert s_1^k\rangle\langle s_1^k\rvert \otimes \lvert s_2^k\rangle\langle s_2^k\rvert$, and any matrix $M$ is uniquely specified by all overlaps with this basis, i.e., by all
$$
c_k(M) = \mathrm{tr}\big[\lvert s_1^k\rangle\langle s_1^k\rvert \otimes \lvert s_2^k\rangle\langle s_2^k\rvert M\big] = \big(\langle s_1^k\rvert \otimes \langle s_2^k\rvert\big) M \big(\lvert s_1^k\rangle\otimes \lvert s_2^k\rangle\big)\ .
$$
Now consider two states $\lvert t\rangle$, $\lvert t'\rangle$, and consider the projectors $M=\lvert t\rangle \langle t\rvert$ and $M'=\lvert t'\rangle \langle t'\rvert$. Thus, if
$$
\left|\big(\langle s_1^k\rvert \otimes \langle s_2^k\rvert\big) \lvert t\rangle \right|^2  =c_k(\lvert t\rangle \langle t\rvert) = c_k(\lvert t'\rangle \langle t'\rvert) =  \left|\big(\langle s_1^k\rvert \otimes \langle s_2^k\rvert\big) \lvert t'\rangle \right|^2 
$$
holds for all $k$, then it follows that $\lvert t\rangle\langle t\rvert = \lvert t'\rangle\langle t'\rvert$, i.e., $\lvert t \rangle$ equals $\lvert t'\rangle$ up to a global phase.
