For those who are interested I give here a slightly more detailed version of Michael's answer.

First note that $T\pi|_{HP} \colon HP \to TB$ is a vector bundle map covering $\pi \colon P \to B$ and a vector space isomorphism on each fiber. This is clear because $T_v\pi$ is obviously onto for every $v \in HP$ and because of dimensional reasons also injective.

Then we can apply Ch. II. 2.26 Prop. XVI from Greub, Halperin, Vanstone: "Connections Curvature and Cohomology Volume I" and get immediately that the map

$$
\alpha \colon C^\infty(P) \otimes_{C^\infty(B)} \Gamma^\infty(TB) \to \Gamma^\infty(HP), f \otimes X \mapsto f \cdot (T\pi|_{HP})^* X
$$

is an isomorphism of $C^\infty(P)$-modules.

Now by the very definition of $(T\pi|_{HP})^*$ and of the horizontal lift, the equation

$$
((T\pi|_{HP})^*X)(p) = T\pi|_{H_vP}^{-1}(X(\pi(p)) = X^h(p)
$$

holds for every $p \in P$ and $X \in \Gamma^\infty(TB)$, i.e. $$(T\pi|_{HP})^* X = X^h$$ for every $X \in \Gamma^\infty(TB)$. Consequently given a $\sigma \in \Gamma^\infty(HP)$ there is a $k \in \mathbb{N}$ and for every $i \in \{1,\dots,k\}$ $f^i \in C^\infty(P)$ and $X_i \in \Gamma^\infty(TB)$ with

$$\sigma = \alpha\left(\sum_{i = 1}^k f^i \otimes X_i\right) = \sum_{i = 1}^k f^i X_i^h.$$

This proves the theorem.

So the only nontrivial part is the proposition from Greub et. al. Just for convenience let my cite it here:

Let $\hat \pi \colon \hat E \to \hat M$ and $\pi \colon E \to M$ be two vector bundles and let $\Phi \colon \hat E \to E$ a vector bundle map over some smooth map $\phi \colon \hat M \to M$ restricting to linear isomorphisms in the fibers. Make $C^\infty(\hat M)$ into an $C^\infty(M)$-module by setting

$$
f \cdot \hat f := \phi^*f \cdot \hat f
$$

for all $f \in C^\infty(M)$ and $\hat f \in C^\infty(\hat M)$. Then the map

$$
\alpha_{\Phi} \colon C^\infty(\hat M) \otimes_{C^\infty(M)} \Gamma^\infty(E) \to \Gamma^\infty(\hat E), \hat f \otimes \sigma \mapsto \hat f \cdot \Phi^* \sigma
$$

is an isomorphism of $C^\infty(\hat M)$-modules. Therby for $\sigma \in \Gamma^\infty(E)$ the smooth section $\Phi^* \sigma \in \Gamma^\infty(\hat E)$ is the pullback of $\sigma$, defined by $(\Phi^*\sigma)(\hat p) := \Phi|_{{\hat E}{\hat p}}^{-1}(\sigma(\hat p))$ for all $\hat p \in \hat M$.

That's essentially the same theorem as Michael stated. Greub et. al. proof it by using that the modules of sections of a vector bundle is finitely generated (Serre-Swan) and that every vector bundle can enlarged via whitney sum to a trivial vector bundle. Again to prove this they also use Serre-Swan.