The koszul formula defines an affine connection

Expand $K(X,Y,fZ)$ using the scalar product rule and [F3]. The derivative-of-$f$ terms, in the order of the six summands, are $(Xf)g(Y,Z)$, $(Yf)g(Z,X)$, $0$, $-(Yf)g(X,Z)$, $-(Xf)g(Y,Z)$, $0$. They cancel by symmetry of $g$, so $K(X,Y,fZ)=fK(X,Y,Z)$. Real linearity and additivity in all three fields follow termwise.

In $K(fX,Y,Z)$ the additional terms are $0$, $(Yf)g(Z,X)$, $-(Zf)g(X,Y)$, $0$, $(Zf)g(Y,X)$, $-(Yf)g(Z,X)$, and hence cancel. Thus $K(fX,Y,Z)=fK(X,Y,Z)$. For $K(X,fY,Z)$ the additional terms are $(Xf)g(Y,Z)$, $0$, $-(Zf)g(X,Y)$, $(Zf)g(X,Y)$, $0$, $(Xf)g(Z,Y)$. Their sum is $2(Xf)g(Y,Z)$, proving $K(X,fY,Z)=fK(X,Y,Z)+2(Xf)g(Y,Z)$.

For fixed local $X,Y$, expand $Z={\sum }_i{Z}^i{\mathrm{\partial }}_i$. Step 1.1 gives $K(X,Y,Z)={\sum }_i{Z}^{i}K(X,Y,{\mathrm{\partial }}_i)$, so $K(X,Y,\cdot )\mathrm{/}2$ is a smooth one-form with those smooth coordinate coefficients. The intrinsic six-term expression shows agreement on overlaps. Apply the smooth map $\mathrm{♯}$ to get the displayed smooth vector field. Nondegeneracy makes it the unique field with $2g({\mathrm{\nabla }}_{X}Y,Z)=K(X,Y,Z)$ for every $Z$.

Step 1.2 and real linearity give function-linearity in $X$, real linearity in $Y$, and ${\mathrm{\nabla }}_X(fY)=f{\mathrm{\nabla }}_{X}Y+(Xf)Y$, since $g(Y,\cdot {)}^{\mathrm{♯}}=Y$. Thus [F4] gives an affine connection. The local formulas agree on restrictions, so they define a global operator without choosing an initial connection. Rank zero and empty base give the unique zero maps; in dimension one the same scalar identities apply. Smooth up-to-boundary functions have the same product and bracket rules in half-space charts, so the argument includes boundary points. Every construction is uniquely determined by the given metric; no AC or partition of unity enters.