[proofplan]
We construct the polar factor first on the range of $|T|$ by sending $|T|x$ to $Tx$. The identity $\||T|x\|_H=\|Tx\|_K$ makes this definition well-defined and isometric, so it extends uniquely to the closure of $\operatorname{Range}(|T|)$. We then set the extension equal to zero on the orthogonal complement, identify the initial and final spaces, and verify $T=U|T|$. The argument applies to every bounded operator between Hilbert spaces; compact operators are a special case.
[/proofplan]
[step:Identify the kernel and initial subspace of $|T|$]
Let
\begin{align*}
A:=|T|=(T^*T)^{1/2}\in\mathcal{L}(H).
\end{align*}
Then $A$ is self-adjoint and non-negative, and $A^2=T^*T$. For every $x\in H$,
\begin{align*}
\|Ax\|_H^2=(Ax,Ax)_H=(A^2x,x)_H=(T^*Tx,x)_H=(Tx,Tx)_K=\|Tx\|_K^2.
\end{align*}
Hence $Ax=0$ if and only if $Tx=0$, so
\begin{align*}
\ker A=\ker T.
\end{align*}
We also identify the closure of the range of $A$. Since $A=A^*$, for $y\in H$,
\begin{align*}
y\in \operatorname{Range}(A)^\perp
\end{align*}
means that $(Az,y)_H=0$ for every $z\in H$. By the adjoint identity, this is equivalent to
\begin{align*}
(z,Ay)_H=0
\end{align*}
for every $z\in H$, hence to $Ay=0$. Therefore
\begin{align*}
\operatorname{Range}(A)^\perp=\ker A.
\end{align*}
Taking orthogonal complements gives
\begin{align*}
\overline{\operatorname{Range}(A)}=(\ker A)^\perp=(\ker T)^\perp.
\end{align*}
[/step]
[step:Define an isometry from $\operatorname{Range}(|T|)$ onto $\operatorname{Range}(T)$]
Define a map
\begin{align*}
U_0:\operatorname{Range}(A)\to \operatorname{Range}(T)
\end{align*}
as follows: for $x\in H$,
\begin{align*}
U_0(Ax):=Tx.
\end{align*}
This is well-defined. Indeed, if $Ax_1=Ax_2$, then $A(x_1-x_2)=0$, so $x_1-x_2\in\ker A=\ker T$, and therefore $Tx_1=Tx_2$.
The map $U_0$ is linear because $A$ and $T$ are linear. Moreover, for every element $Ax\in\operatorname{Range}(A)$,
\begin{align*}
\|U_0(Ax)\|_K=\|Tx\|_K=\|Ax\|_H.
\end{align*}
Thus $U_0$ is an isometry from $\operatorname{Range}(A)$ onto $\operatorname{Range}(T)$.
[guided]
The natural way to recover $T$ from $|T|$ is to define the missing factor by the rule that it should send $|T|x$ to $Tx$. We therefore define
\begin{align*}
U_0:\operatorname{Range}(A)\to \operatorname{Range}(T)
\end{align*}
by
\begin{align*}
U_0(Ax):=Tx
\end{align*}
for $x\in H$.
The first point to check is well-definedness. We first recall why $\ker A=\ker T$. Since $A^2=T^*T$, for every $x\in H$,
\begin{align*}
\|Ax\|_H^2=(Ax,Ax)_H=(A^2x,x)_H=(T^*Tx,x)_H=(Tx,Tx)_K=\|Tx\|_K^2.
\end{align*}
Hence $Ax=0$ if and only if $Tx=0$, so $\ker A=\ker T$.
Now the same vector in $\operatorname{Range}(A)$ may have two representations, say $Ax_1=Ax_2$. Then
\begin{align*}
A(x_1-x_2)=0.
\end{align*}
Using $\ker A=\ker T$, we get $x_1-x_2\in\ker T$. Hence
\begin{align*}
Tx_1-Tx_2=T(x_1-x_2)=0,
\end{align*}
and therefore $Tx_1=Tx_2$. Thus the value $U_0(Ax)$ depends only on $Ax$, not on the chosen preimage $x$.
Linearity follows from the linearity of $A$ and $T$. If $a,b$ are scalars and $x_1,x_2\in H$, then
\begin{align*}
U_0(aAx_1+bAx_2)=U_0(A(ax_1+bx_2))=T(ax_1+bx_2)=aTx_1+bTx_2.
\end{align*}
Since $U_0(Ax_i)=Tx_i$ for $i=1,2$, this proves linearity on $\operatorname{Range}(A)$.
Finally, $U_0$ preserves norms. For every $x\in H$, the identity from the previous step gives
\begin{align*}
\|U_0(Ax)\|_K=\|Tx\|_K=\|Ax\|_H.
\end{align*}
Therefore $U_0$ is an isometry on $\operatorname{Range}(A)$. Its range is exactly $\operatorname{Range}(T)$, because every element of $\operatorname{Range}(T)$ has the form $Tx=U_0(Ax)$.
[/guided]
[/step]
[step:Extend the isometry and set it to zero on the orthogonal complement]
We define the extension directly. Let $m\in\overline{\operatorname{Range}(A)}$. Choose a sequence $(m_j)_{j=1}^{\infty}$ in $\operatorname{Range}(A)$ such that $m_j\to m$ in $H$. Since $U_0$ is an isometry, $(U_0m_j)_{j=1}^{\infty}$ is a [Cauchy sequence](/page/Cauchy%20Sequence) in $K$. Since $K$ is complete because $K$ is a [Hilbert space](/page/Hilbert%20Space), there is a unique vector in $K$ denoted by $Vm$ such that
\begin{align*}
U_0m_j\to Vm.
\end{align*}
This definition is independent of the approximating sequence: if $(m_j')_{j=1}^{\infty}$ is another sequence in $\operatorname{Range}(A)$ with $m_j'\to m$ in $H$, then
\begin{align*}
\|U_0m_j-U_0m_j'\|_K=\|m_j-m_j'\|_H\to 0,
\end{align*}
so both image sequences have the same limit. Thus we obtain a map
\begin{align*}
V:\overline{\operatorname{Range}(A)}\to K
\end{align*}
which satisfies $V(Ax)=Tx$ for every $x\in H$ by taking the constant approximating sequence $m_j=Ax$. The map $V$ is linear: if $m,n\in\overline{\operatorname{Range}(A)}$ and $a,b$ are scalars, choose sequences $(m_j)_{j=1}^{\infty}$ and $(n_j)_{j=1}^{\infty}$ in $\operatorname{Range}(A)$ with $m_j\to m$ and $n_j\to n$ in $H$; then $am_j+bn_j\to am+bn$ in $H$, and linearity of $U_0$ gives
\begin{align*}
V(am+bn)=\lim_{j\to\infty}U_0(am_j+bn_j)=aVm+bVn.
\end{align*}
The extension $V$ is an isometry on $\overline{\operatorname{Range}(A)}$: for $m\in\overline{\operatorname{Range}(A)}$ and $m_j\to m$ in $\operatorname{Range}(A)$,
\begin{align*}
\|Vm\|_K=\lim_{j\to\infty}\|U_0m_j\|_K=\lim_{j\to\infty}\|m_j\|_H=\|m\|_H.
\end{align*} Since $V$ agrees with $U_0$ on $\operatorname{Range}(A)$, we have $\operatorname{Range}(T)\subset \operatorname{Range}(V)$. Conversely, if $m\in\overline{\operatorname{Range}(A)}$, choose a sequence $(m_j)_{j=1}^{\infty}$ in $\operatorname{Range}(A)$ with $m_j\to m$ in $H$. Continuity of $V$ gives $V m_j\to V m$ in $K$, and each $V m_j$ lies in $\operatorname{Range}(T)$. Hence $V m\in\overline{\operatorname{Range}(T)}$.
We now prove that $\operatorname{Range}(V)$ is closed in $K$. Let $(Vm_j)_{j=1}^{\infty}$ be a sequence in $\operatorname{Range}(V)$ converging in $K$ to some $y\in K$, where each $m_j\in\overline{\operatorname{Range}(A)}$. Since $V$ is an isometry, $(m_j)_{j=1}^{\infty}$ is a Cauchy sequence in the Hilbert space $\overline{\operatorname{Range}(A)}$. Therefore $m_j\to m$ in $H$ for some $m\in\overline{\operatorname{Range}(A)}$, and continuity of $V$ gives $Vm=y$. Thus $y\in\operatorname{Range}(V)$, so $\operatorname{Range}(V)$ is closed. Combining the two inclusions with closedness gives
\begin{align*}
\operatorname{Range}(V)=\overline{\operatorname{Range}(T)}.
\end{align*}
Using the [orthogonal decomposition](/theorems/436)
\begin{align*}
H=\overline{\operatorname{Range}(A)}\oplus \overline{\operatorname{Range}(A)}^\perp,
\end{align*}
define
\begin{align*}
U:H\to K
\end{align*}
by
\begin{align*}
U(m+n):=Vm
\end{align*}
for $m\in\overline{\operatorname{Range}(A)}$ and $n\in\overline{\operatorname{Range}(A)}^\perp$. This operator is linear and bounded, with
\begin{align*}
\|U(m+n)\|_K=\|Vm\|_K=\|m\|_H\leq \|m+n\|_H.
\end{align*}
Thus $U\in\mathcal{L}(H,K)$.
[/step]
[step:Verify that $U$ is the required partial isometry]
By construction, $U$ is an isometry on
\begin{align*}
\overline{\operatorname{Range}(A)}=(\ker T)^\perp
\end{align*}
and $U=0$ on its orthogonal complement. Since
\begin{align*}
\overline{\operatorname{Range}(A)}^\perp=\ker T,
\end{align*}
and since the previous step proved $\operatorname{Range}(V)=\overline{\operatorname{Range}(T)}$, the operator $U$ is a partial isometry with initial space $(\ker T)^\perp$ and final space $\overline{\operatorname{Range}(T)}$.
For every $x\in H$, the vector $Ax$ belongs to $\operatorname{Range}(A)$, so the defining property of the extension gives
\begin{align*}
U|T|x=UAx=V(Ax)=Tx.
\end{align*}
Therefore
\begin{align*}
T=U|T|.
\end{align*}
[/step]
[step:Prove uniqueness on $(\ker T)^\perp$ under the zero-on-kernel convention]
Let $W\in\mathcal{L}(H,K)$ be another partial isometry with initial space $(\ker T)^\perp$ such that
\begin{align*}
T=W|T|.
\end{align*}
For every $x\in H$,
\begin{align*}
W(Ax)=Tx=U(Ax).
\end{align*}
Thus $W$ and $U$ agree on $\operatorname{Range}(A)$. Since both operators are continuous and
\begin{align*}
\overline{\operatorname{Range}(A)}=(\ker T)^\perp,
\end{align*}
they agree on $(\ker T)^\perp$.
Under the standard convention, both operators are set equal to zero on $\ker T$, the orthogonal complement of the initial space. Hence the standard polar factor is uniquely determined by $T$. This completes the proof.
[/step]