Theorem: Space of Compact Linear Transformations is Banach Space

Let $\GF \in \set {\R,\C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space over $\GF$.
Let $\struct {Y, \norm {\, \cdot \,}_Y}$ be a Banach space oer $\GF$.
Let $\map \KK {X, Y}$ be the space of compact linear transformations from $H$ to $K$.
Now $\map \KK {X, Y} \subseteq Y^X$, where $Y^X$ is the set of mappings from $X$ to $Y$.
Therefore, $\map \KK {X, Y}$ can be endowed with pointwise addition ($+$) and ($\GF$)-scalar multiplication ($\circ$).
Let $\norm {\, \cdot \,}_{\map \BB {X, Y} }$ denote the norm on bounded linear operators.
Let $\norm {\, \cdot \,}_{\map \KK {X, Y} }$ be the restriction of $\norm {\, \cdot \,}_{\map \BB {X, Y} }$ to $\map \KK {X, Y}$.
Then $\norm {\, \cdot \,}_{\map \KK {X, Y} }$ is a norm on $\map \KK {X, Y}$.
Furthermore, $\map \KK {X, Y}$ is a Banach space with respect to this norm.

Proof:
First, from Restriction of Norm on Vector Space to Subspace is Norm, $\norm {\, \cdot \,}_{\map \KK {X, Y} }$ is a norm on $\map \KK {X, Y}$.
Now, we prove that $\map \KK {X, Y}$ is a closed vector subspace of $\map \BB {X, Y}$.
First, from Zero Linear Transformation is Compact, $\map \KK {X, Y} \ne \O$. 
To then prove that $\map \KK {X, Y}$ is a vector subspace of $\map \BB {X, Y}$, it is enough to prove that:
:for all $T_1, T_2 \in \map \KK {X, Y}$ and $\lambda \in \GF$, we have that $T_1 + \lambda T_2 \in \map \KK {X, Y}$
from One-Step Vector Subspace Test.
This is given by Linear Combination of Compact Linear Transformations is Compact.
We now need to prove that $\map \KK {X, Y}$ is closed in $\map \BB {X, Y}$.
Let $\sequence {T_n}_{n \mathop \in \N}$ be a convergent sequence in $\map \KK {X, Y}$ with limit $T \in \map \BB {X, Y}$.
We show that $T \in \map \KK {X, Y}$.
Let $\cl$ be the topological closure.
Let $B_X^-$ be the closed unit ball in $\struct {X, \norm {\, \cdot \,}_X}$.
Since $T_n$ is compact for each $n \in \N$, we have that:
:$\map \cl {T_n \sqbrk {B_X^-} }$ is compact for each $n \in \N$. 
From Compact Metric Space is Totally Bounded, we have that:
:$\map \cl {T_n \sqbrk {B_X^-} }$ is totally bounded for each $n \in \N$. 
From Subspace of Complete Metric Space is Relatively Compact iff Totally Bounded, it is enough to show that:
:$T \sqbrk {B_X^-}$ is totally bounded
since $Y$ is Banach.
Let $\epsilon > 0$. 
We can find $N \in \N$ such that:
:$\ds \norm {T_N - T}_{\map \BB {X, Y} } < \frac \epsilon 2$ 
For this $N$, take $x_1, \ldots, x_n \in T_N \sqbrk {B_X^-}$ such that:
:$\ds T_N \sqbrk {B_X^-} \subseteq \bigcup_{i \mathop = 1}^n \map {B_{\epsilon/2} } {\map {T_N} {x_i} }$
Now let $x \in B_X^-$. 
Pick $1 \le i \le n$ such that: 
:$\ds \norm {T_N x - T_N x_i}_Y < \epsilon/2$. 
Since:
:$\ds \norm {T_N - T}_{\map \BB {X, Y} } < \frac \epsilon 2$ 
we have that:
:$\ds \norm {T x - T_N x}_Y < \frac \epsilon 2$
Hence:
{{begin-eqn}}
{{eqn	| l = \norm {T x - T x_i}_Y
		| o = \le
		| r = \norm {T x - T_N x}_Y + \norm {T_N x - T_N x_i}_Y
		| c = {{NormAxiomVector|3}}
}}
{{eqn	| o = <
		| r = \frac \epsilon 2 + \frac \epsilon 2 
		| c = {{Defof|Norm on Bounded Linear Transformation}}
}}
{{eqn	| r = \epsilon 
}}
{{end-eqn}}
Hence:
:$\ds T \sqbrk {B_X^-} \subseteq \bigcup_{i \mathop = 1}^n \map {B_\epsilon} {T x_i}$
where $T x_1, \ldots, T x_n \in T \sqbrk {B_X^-}$.
Since $\epsilon > 0$ was arbitrary, we have that $T \sqbrk {B_X^-}$ is relatively compact by Subspace of Complete Metric Space is Relatively Compact iff Totally Bounded, since $Y$ is Banach.
That is, $\map \cl {T \sqbrk {B_X^-} }$ is compact.
Hence, $T$ is compact.
Hence $\map \KK {X, Y}$ is closed in $\map \BB {X, Y}$.
From Space of Bounded Linear Transformations is Banach Space, $\map \BB {X, Y}$ is a Banach space.
From Closed Subspace of Banach Space forms Banach Space, $\map \KK {X, Y}$ is a Banach space.
{{qed}}