Finite ultraproduct I stucked when trying to prove:
If $A_\xi$ are domains of models of first order language and $|A_\xi|\le n$ for $n \in \omega$ for all $\xi$ in index set $X$ and $\mathcal U$ is ultrafilter of $X$ then $|\prod_{\xi \in X} A_\xi / \mathcal U| \le n$.
My tries:
If $X$ is finite set then $\mathcal U$ is principal. Then singleton $\{x\}\in \mathcal U$ and $|\prod_{\xi \in X} A_\xi / \mathcal U| = |A_x|$. If $\mathcal U$ is not principal then for $x \in X$ there is $S_x \in \mathcal U$ with $x \notin S_x$. Then for every $k \in \omega$ there exists equivalence class corresponding to $S_{x_1} \cap \dots \cap S_{x_k}$ with size greater $|A_1|\cdot \dots \cdot |A_k|$. 
Can there be said anything about a structure of the ultrafilter if $X$ is infinite? And how to prove it?

For $k=1,2,3,\dots, n$, let $X_k$ be the set of all $\xi\in X$ such that $|A_{\xi}|=k$. 
Since $X$ is the finite disjoint union $X_1\cup X_2\cup \cdots \cup X_n$, there is precisely one value of $k$ such that $X_k\in \mathcal{U}$. The ultrapower then has $k$ elements.   
Why does it have $k$ elements? We can think in terms of sentences: the assertion that there are precisely $k$ elements  is true "almost everywhere" modulo $\mathcal{U}$. 
The following is a perhaps somewhat more concrete reason, if the word concrete can be applied to ultrafilters. Work over the $X_k$ which is in $\mathcal{U}$. For $\xi\in X_k$, we can assume that $A_{\xi}$ consists of the numbers $1,2,\dots,k$. Then any element of the product $\prod A_{\xi}$ is almost everywhere (modulo $\mathcal{U}$) equal to one of the sequences of all $1$'s, all $2$'s, and so on up to all $k$'s.  
