Trace is absolutely convergent and basis independent

The candidate scalar is absolutely convergent. For a nuclear representation, $\mathrm{\mid }⟨v_j,u_j⟩\mathrm{\mid }\le \mathrm{\parallel }{u}_j\mathrm{\parallel }\mathrm{\parallel }{v}_j\mathrm{\parallel }$ by [A4], so the scalar series converges absolutely with $\mathrm{\mid }{\sum }_j⟨v_j,u_j⟩\mathrm{\mid }\le {\sum }_j\mathrm{\parallel }{u}_j\mathrm{\parallel }\mathrm{\parallel }{v}_j\mathrm{\parallel }$ by [A2].

Comparison of two representations. Put $K_0:=\stackrel{}{\mathrm{span}}(\{u_j\}\cup \{u_j^{\mathrm{\prime }}\}\cup \{v_j\}\cup \{v_j^{\mathrm{\prime }}\})$, listing the finitely many zero families as the constant zero sequence when necessary. Let ${\mathbb{F}}_0:=\mathbb{Q}$ when $H$ is real and ${\mathbb{F}}_0:=\mathbb{Q}(i)$ when $H$ is complex. Then $K_0$ is a closed subspace with the at most countable dense set of all finite ${\mathbb{F}}_0$-linear combinations of the listed vectors (which exists without choice), so by [A3] it has a finite or countable Hilbert basis $(g_n{)}_{n\in N}$ obtained from that sequence by Gram–Schmidt. Both representations show $T(K_0)\subseteq K_0$ (the value at $x\in K_0$ is a norm limit of combinations of the $v_j$, respectively $v_j^{\mathrm{\prime }}$) and $Tx=0$ for $x\perp K_0$ (all coefficients $⟨x,u_j⟩$, $⟨x,u_j^{\mathrm{\prime }}⟩$ vanish). For the representation $R$, expanding both factors in the basis $(g_n)$ by Parseval [A3] and using absolute convergence and the interchange of nonnegative finite-subset suprema [A2], ${\sum }_j⟨v_j,u_j⟩={\sum }_j{\sum }_n⟨v_j,g_n⟩⟨g_n,u_j⟩={\sum }_n{\sum }_j⟨v_j,g_n⟩⟨g_n,u_j⟩={\sum }_n⟨T{g}_n,g_n⟩$, the inner identity because $T{g}_n={\sum }_j⟨g_n,u_j⟩v_j$ in norm. The same computation applies to $R^{\mathrm{\prime }}$, so both representations have the same scalar sum; since a trace-class operator has at least one nuclear representation by [A1], the scalar $\mathrm{tr}(T):={\sum }_j⟨v_j,u_j⟩$ is well defined and claim 2 holds.

Agreement with every supplied basis. Let $E$ be a Hilbert basis of $H$ and let $R=((u_j),(v_j))$ be any nuclear representation of $T$. For each $j$, Parseval in the full space gives $\mathrm{\parallel }{u}_j{\mathrm{\parallel }}^2={\sum }_{e\in E}\mathrm{\mid }⟨u_j,e⟩{\mathrm{\mid }}^2$ and $\mathrm{\parallel }{v}_j{\mathrm{\parallel }}^2={\sum }_{e\in E}\mathrm{\mid }⟨v_j,e⟩{\mathrm{\mid }}^2$; hence, by Cauchy–Schwarz for the $e$-sum, interchange of the nonnegative suprema [A2] and the definition of the representation, ${\sum }_{e\in E}{\sum }_j\mathrm{\mid }⟨e,u_j⟩\mathrm{\mid }\mathrm{\mid }⟨v_j,e⟩\mathrm{\mid }\le {\sum }_j\mathrm{\parallel }{u}_j\mathrm{\parallel }\mathrm{\parallel }{v}_j\mathrm{\parallel }<+\mathrm{\infty }$. Therefore the double sum ${\sum }_e{\sum }_j⟨e,u_j⟩⟨v_j,e⟩$ converges absolutely, its value may be computed in either order, and ${\sum }_{e\in E}⟨Te,e⟩={\sum }_{e\in E}{\sum }_j⟨e,u_j⟩⟨v_j,e⟩={\sum }_j{\sum }_{e\in E}⟨e,u_j⟩⟨v_j,e⟩={\sum }_j⟨v_j,u_j⟩$, the last equality by Parseval applied to the pair $(v_j,u_j)$ in $H$. This is exactly ${\mathrm{tr}}_E(T)=\mathrm{tr}(T)$, and it also reproves the absolute summability of $(⟨Te,e⟩)$ required by the definition.

Linearity and the bound. For trace-class $S,T$ with nuclear representations $R_S$ and $R_T$, the concatenation of $R_S$ scaled by $a$ and $R_T$ scaled by $b$ is a nuclear representation of $aS+bT$ with scalar sum $a\sum ⟨v_j,u_j⟩+b\sum ⟨v_j^{\mathrm{\prime }},u_j^{\mathrm{\prime }}⟩$ by absolute convergence, so $\mathrm{tr}(aS+bT)=a\mathrm{tr}(S)+b\mathrm{tr}(T)$; and $\mathrm{\mid }\mathrm{tr}(T)\mathrm{\mid }\le {\sum }_j\mathrm{\parallel }{u}_j\mathrm{\parallel }\mathrm{\parallel }{v}_j\mathrm{\parallel }$ for every nuclear representation by [step 1.1], so the infimum characterization [A1] gives $\mathrm{\mid }\mathrm{tr}(T)\mathrm{\mid }\le \mathrm{\parallel }T{\mathrm{\parallel }}_1$.

Conclusion. Claims 1 and 2 are [step 1.1] and [step 1.2], claim 3 is [step 1.3] and claim 4 is [step 2.1]; the definition of $\mathrm{tr}(T)$ uses only nuclear representations of $T$, so no Hilbert basis of $H$ is assumed to exist, while claim 3 handles every basis that is supplied.