Assuming countable choice, the semifinite part is a semifinite measure and equals the original measure exactly when it is semifinite

One has ${\mu }_{\mathrm{s}\mathrm{f}}(\mathrm{\varnothing })=0$ and ${\mu }_{\mathrm{s}\mathrm{f}}(E)\le \mu (E)$ for every measurable $E$, since every finite-measure $F\subseteq E$ satisfies $\mu (F)\le \mu (E)$.

Let $(E_k)$ be disjoint and $E={\bigcup }_k{E}_k$. If $F\subseteq E$ is measurable with $\mu (F)<+\mathrm{\infty }$, then the $F\cap E_k$ are disjoint finite-measure subsets of $E_k$, so $\mu (F)={\sum }_k\mu (F\cap E_k)\le {\sum }_k{\mu }_{\mathrm{s}\mathrm{f}}(E_k)$. Taking the supremum over $F$ gives ${\mu }_{\mathrm{s}\mathrm{f}}(E)\le {\sum }_k{\mu }_{\mathrm{s}\mathrm{f}}(E_k)$.

Conversely, for each finite initial range, the supremum property and finite choice permit finite-measure $F_k\subseteq E_k$ arbitrarily close to ${\mu }_{\mathrm{s}\mathrm{f}}(E_k)$; their finite disjoint union has finite measure and lies in $E$. If one of the finitely many suprema is $+\mathrm{\infty }$, use an arbitrarily large finite value instead. Hence every finite partial sum ${\sum }_{k<n}{\mu }_{\mathrm{s}\mathrm{f}}(E_k)$ is at most ${\mu }_{\mathrm{s}\mathrm{f}}(E)$, and so is their supremum.

The set function ${\mu }_{\mathrm{s}\mathrm{f}}$ is semifinite: if ${\mu }_{\mathrm{s}\mathrm{f}}(E)>0$, its defining supremum supplies a measurable $F\subseteq E$ with $0<\mu (F)<+\mathrm{\infty }$, and then ${\mu }_{\mathrm{s}\mathrm{f}}(F)=\mu (F)$.

For the reverse direction, suppose $\mu$ is semifinite. If $\mu (E)<+\mathrm{\infty }$, the choice $F=E$ gives ${\mu }_{\mathrm{s}\mathrm{f}}(E)=\mu (E)$; if $\mu (E)=+\mathrm{\infty }$, [L2] makes the defining finite values unbounded, so again ${\mu }_{\mathrm{s}\mathrm{f}}(E)=\mu (E)$.

Steps 1.1, 1.2 and 1.3 give the empty-set condition and both countable-additivity inequalities, so ${\mu }_{\mathrm{s}\mathrm{f}}$ is a measure; step 1.4 makes it semifinite.

For the forward direction of the displayed equivalence, if ${\mu }_{\mathrm{s}\mathrm{f}}=\mu$, then $\mu$ is semifinite because step 2.1 proves that ${\mu }_{\mathrm{s}\mathrm{f}}$ is semifinite.

Steps 3.1 and 1.5 prove both directions of the equivalence, while step 1.1 records the pointwise inequality ${\mu }_{\mathrm{s}\mathrm{f}}\le \mu$.