It follows from [Ber93, Theorem 1.6.1] that the base change of $V$ to $F$ is a paracompact strictly $F$-analytic space. Property (a) is obvious.

To prove (b), we assume that ${\|\hskip 4.30554pt\|}$ is a piecewise linear metric on $L\hat{\otimes}_{K}F$. We have seen in 2.2 that $(V,L)$ has a formal ${K^{\circ}}$-model $({\mathfrak{V}},{\mathfrak{L}})$ and so we may assume that $L={\mathcal{O}}_{V}$ by passing to ${\|\hskip 4.30554pt\|}/{\|\hskip 4.30554pt\|}_{{\mathfrak{L}}\hat{\otimes}_{{K^{\circ}}}F^{\circ}}$. By Proposition 2.8, there is a formal $F^{\circ}$-model $({\mathfrak{V}}^{\prime\prime},{\mathfrak{L}}^{\prime\prime})$ of $(V\hat{\otimes}_{K}F,L\hat{\otimes}_{K}F)$ such that ${\|\hskip 4.30554pt\|}={\|\hskip 4.30554pt\|}_{{\mathfrak{L}}^{\prime\prime}}$. By Raynaud’s theorem [BL93a, Theorem 4.1], we may assume that there is an admissible formal blowing up ${\mathfrak{V}}^{\prime\prime}\to{\mathfrak{V}}\hat{\otimes}_{{K^{\circ}}}F^{\circ}$. Note that $L={\mathcal{O}}_{V}$ yields that ${\mathfrak{L}}^{\prime\prime}={\mathcal{O}}(E)$ for a vertical Cartier divisor $E$ on ${\mathfrak{V}}^{\prime\prime}$. Replacing ${\|\hskip 4.30554pt\|}$ by a suitable multiple, we may assume that $E$ is an effective Cartier divisor.

An approximation argument based on the density of the algebraic closure of $K$ in $F$ shows that the coherent ideal of the admissible formal blowing up and hence the formal model ${\mathfrak{V}}^{\prime\prime}$ are defined on a formal $(K^{\prime})^{\circ}$-model ${\mathfrak{V}}^{\prime}$ for a finite subextension $K^{\prime}/K$ of $F/K$. We choose a finite covering $({\mathfrak{U}}_{i}^{\prime})_{i\in I}$ of ${\mathfrak{V}}^{\prime}$ by formal affine open subsets ${\mathfrak{U}}_{i}^{\prime}$ of ${\mathfrak{V}}^{\prime}$. Then the coherent sheaf of ideals ${\mathcal{O}}(-E^{\prime\prime})$ restricted to ${\mathfrak{U}}_{i}^{\prime}\hat{\otimes}_{(K^{\prime})^{\circ}}F^{\circ}$ is generated by finitely many regular functions. A similar approximation argument as above shows that all these generators can be replaced by regular functions on ${\mathfrak{U}}_{i}^{\prime}$ if we replace $K^{\prime}$ by a larger finite subextension of $F/K$. We conclude that ${\mathfrak{L}}^{\prime\prime}={\mathcal{O}}(E)$ is defined on ${\mathfrak{V}}^{\prime}$ proving (b). Note that uniqueness is obvious. ∎