The state space of the stabilization of a C*-algebra

From the general point of view of $C^*$-algebra theory, Bill Paschke mentioned to me today an interesting classification of states (or even, positive functionals) on the stabilization of $A$ as follows:

Proposition. Let $A$ be unital $C^{ast}$-algebra, $H$ be a Hilbert space and $varphi$ be a positive linear functional on $Aotimesmathcal{K}(H)$. Let ${cal L}^1(H)$ denote the ideal of trace-class operators on $H$. Then there exist a Hilbert space $H_{varphi}$, a representation $pi:Arightarrow B(H_varphi)$ and an operator $S:Hrightarrow H_{varphi}$ such that $S^*Sin{cal L}^1(H)$ (so $S^{ast}pi(a),Sinmathcal{L}^1(H)$ for $ain A$), and $varphi(aotimes K)={rm tr}(S^{ast}pi(a),S,K)$ for all $ain A$ and $Kinmathcal{K}(H)$.
Moreover, $varphi$ is a state iff ${rm tr}(S^{ast}S)=1$.

Proof. Since ${cal K}(H)^{ast}cong{cal L}^1(H)$, any positive linear functional $varphi$ can be regarded as a completely positive map $T:Arightarrow{cal L}^1(H)$ with $varphi(aotimes K)={rm tr}(T(a)K)$. Define a sesquilinear form on the algebraic tensor
product $Aodot H$ by $$langle aotimesxi,botimesetarangle_{varphi}:=langle T(b^{ast}a)xi,etarangle_{H},$$ set $N_{varphi}={rm span}{aotimesxiin Aodot Hmidlangle T(a^{ast}a)xi,xirangle_{H}=0}$ and $H_{varphi}:=overline{Aodot H/N_{varphi}}$. Then we can define a representation $pi:Arightarrow B(H_varphi)$ by
$$pi(a)(botimeseta+N_{varphi}):=abotimeseta+N_{varphi}.$$ Now, let $S:Hrightarrow H_{varphi}$ be the operator defined by $$Sxi:=1otimesxi+N_{varphi}.$$ Then $S^{ast}:H_{varphi}rightarrow H$ is given by $$S^{ast}(botimeseta+N_{varphi})=T(b)eta,$$ and we have $S^{ast}S=T(1)in{cal L}^1(H)$. Moreover, $S^{ast}pi(a),S=T(a)$,
which is what we need. It is easy to see that $||varphi||={rm tr}(S^{ast}S)$. Q.E.D