Concise argument: $[f]$ in the ultrafilter that realizes $\Sigma$? Let $\mathcal{L}$ be a countable language and $\mathcal{A}_i$ be $\mathcal{L}$-structures.
Let $\mathcal{A}=\prod_{i \in \omega} \mathcal{A}_i/\mathcal{U}$, where $\mathcal{U}$ is a non-principal ultrafilter.
Let $S=\{[f_k]:k \in \omega\}$ where $[f_i] \neq [f_j] \in A$ when $i \neq j$.
Let $\Sigma(u)$ be a complete 1-type of $T=Th(\mathcal{A}_S)$, where $\mathcal{A}_S$ is the corresponding structure to $\mathcal{A}$ in the language obtained by adding one constant symbol for each element of $S$.

Q: Can we find a $[f] \in A$ that realizes $\Sigma$?

I am still new to ultrafilters, so I would like to do this from scratch as much as possible, not citing theorems except one's that I've already proven. I know Los's Theorem (although I don't know if it helps here) and I know that a non-principal ultrafilter must contain all the cofinite sets, but that's about it. Also I would like to do this as concisely as possible, hopefully with an argument that takes half a page or so.
 A: Assume WLOG that the $\mathcal{A}_i$s are disjoint. Changing notation a bit, I'll write "$\mathcal{A}^S$" for your "$\mathcal{A}_S$." The reason for this notational change is that it lets us more cleanly emulate the same construction on the level of the individual factors: let $\mathcal{A}_i^S$ be the expansion of $\mathcal{A}_i$ by a constant symbol $c_k$ naming $f_k(i)$, for each $k\in\omega$. Note that we have $\mathcal{A}^S=\prod\mathcal{A}^S_i/\mathcal{U}$.
Now the idea is that a sequence of elements of the $\mathcal{A}_i^S$s $g$ getting better and better at realizing $\Sigma(u)$ in the individual $\mathcal{A}_i^S$s translates to $[g]_\mathcal{U}$ as an element of the ultraproduct actually realizing all of $\Sigma(u)$ in the ultraproduct. Fix some enumeration of the formulas in $\Sigma(u)$. Given $i\in\omega$ and $a\in\mathcal{A}_i^S$, say that the $i$-goodness of $a$ is the largest $n\in\omega+1$ such that $a$ realizes in $\mathcal{A}^S_i$ the first $n$ formulas in $\Sigma(u)$. Note that for each $i\in\omega$ we can find an $a_i\in\mathcal{A}_i^S$ such that either the $i$-goodness of $a_i$ is $\ge i$, or the $i$-goodness of $a_i$ is maximal amongst all elements of $\mathcal{A}_i^S$; let $g$ be a sequence whose $i$th term is such an $a_i$.
At this point you can show that, for each formula $\varphi\in\Sigma(u)$, $\mathcal{U}$-many $i$s have $g(i)$ realizing $\varphi$ in $\mathcal{A}_i^S$. Los' Theorem then tells us that $[g]_\mathcal{U}$ realizes $\Sigma(u)$ in $\mathcal{A}^S$. This may be easier to see if you first consider the case of an ultrapower, that is, an ultraproduct where all the $\mathcal{A}_i$s are isomorphic; this has the benefit of guaranteeing that we can always find arbitrarily high $i$-goodness elements of $\mathcal{A}_i^S$.
