Some times ago I posted [this](https://mathoverflow.net/questions/32138/reference-for-some-elementary-facts-about-principal-bundles) question here. There I carelessly assumed that if you have a set of sections of a vector bundle which span every fiber pointwise, they also generate the module of smooth sections over the smooth functions on the base manifold, I think that is true if your set of sections is finite. But in my situation for the horizontal bundle this is not the case. So I want to ask the following question:


Let $(P,\pi,B,G)$ be a principal bundle with total space $P$, base $B$, projection $\pi$ and structure group $G$. Let $\gamma \colon TP \to \mathrm{Lie}(G)$ a connection one-form, which induces the horizontal space $HP$. For a vector field $X \in \Gamma^\infty(TB)$ I write $X^h \in \Gamma^\infty(HP)$ for the horizontal lift of $X$ with respect to $\gamma$. 


Is it true that $\Gamma^\infty(HP) = C^\infty(P)-\mathrm{Span}(X^h \mid X \in \Gamma^\infty(TB))$, i.e. that the horizontal lifts generate the $C^\infty(P)$-module of horizontal vector fields. 


If so, can you give me a proof?


(For a vector bundle $E \to M$ I denote the smooth sections on $E$ by $\Gamma^\infty(E)$. $C^\infty(M)$ are the smooth functions on the manifold $M$)


Note that every manifold is assumed to be real, finite dimensional, $T\_2$, paracompact and smooth.



module of sections of the horizontal bundle
There is a result (for which I don't recall a reference, but you might prove it maybe with the smooth Serre-Swan theorem. See for example Nestruev, Smooth manifolds and observables), which says that for the sections of the pullback of a vector bundle $E\to M$ along a map $\phi:N\to M$ one has 
$$\Gamma(\phi^\*(E))=C^\infty(N)\otimes\_{C^\infty(M)}\Gamma (E)$$
This is a canonical isomorphism obtained from the natural map $\Gamma(E)\to\Gamma(\phi^\*(E))$. Combining this with the fact that the horizontal bundle in your case is canonically isomorphic with the pullback of $TB$ to $P$ would give you a proof.


