The Bott partial connection is well defined and flat along leaves

In any quotient-bundle frame a local lift of $s$ is obtained by using the same smooth coefficient functions in lifted frame vectors. Two such local representatives of $s$ differ by a section $\sigma ={\tilde{s}}^{\mathrm{\prime }}-\tilde{s}\in \mathrm{\Gamma }(E)$, and since $E$ is integrable it is involutive by [F2], so $[X,\sigma ]\in \mathrm{\Gamma }(E)$ and $[X,{\tilde{s}}^{\mathrm{\prime }}]=[X,\tilde{s}]+[X,\sigma ]$; applying the quotient map $\pi$ of [F1] kills $[X,\sigma ]$, so $\pi [X,{\tilde{s}}^{\mathrm{\prime }}]=\pi [X,\tilde{s}]$ and ${\mathrm{\nabla }}_X^{B}s$ is independent of the chosen local representative. Consequently these smooth local sections agree on overlaps and define a global section.

For $f\in C^{\mathrm{\infty }}(M)$ the first Leibniz rule of [F3] gives $[fX,\tilde{s}]=f[X,\tilde{s}]-(\tilde{s}f)X$, and the correction $(\tilde{s}f)X$ is a section of $E$, so projecting gives ${\mathrm{\nabla }}_{fX}^{B}s=f{\mathrm{\nabla }}_X^{B}s$, that is, $C^{\mathrm{\infty }}(M)$-linearity in the vector-field variable.

The second Leibniz rule of [F3] gives $[X,f\tilde{s}]=f[X,\tilde{s}]+X(f)\tilde{s}$ for the representative $f\tilde{s}$ of $fs$, so projecting yields ${\mathrm{\nabla }}_X^B(fs)=f{\mathrm{\nabla }}_X^{B}s+X(f)s$, the stated Leibniz rule.

For flatness, lift ${\mathrm{\nabla }}_Y^{B}s=\pi [Y,\tilde{s}]$ locally by $[Y,\tilde{s}]$ and compute ${\mathrm{\nabla }}_X^B{\mathrm{\nabla }}_Y^{B}s-{\mathrm{\nabla }}_Y^B{\mathrm{\nabla }}_X^{B}s-{\mathrm{\nabla }}_{[X,Y]}^{B}s=\pi ([X,[Y,\tilde{s}]]-[Y,[X,\tilde{s}]]-[[X,Y],\tilde{s}])$; the bracketed expression is the Jacobi identity of [F4] applied to $X,Y,\tilde{s}$, hence vanishes, and well-definedness from step 1.1 makes the result independent of all lifts, so $R^B(X,Y)s=0$ and the connection is flat along leaf directions; only the stated bracket and involutivity facts were used, with no additional choice principle.