Set ultraproducts and constant-map ultrapowers

Work in ZFC. Let $({\mathcal{M}}_i{)}_{i\in I}$ be a set family of nonempty structures in one set signature with finite-arity symbols, as in Structures and variable assignments, and U a proper Ultrafilter on nonempty I. The Axiom of Choice supplies an element of the product of carriers. For product functions f,g put

$f{\sim }_{U}g⟺\{i:f(i)=g(i)\}\in U\mathrm{.}$

The ultraproduct has carrier $({\prod }_i{M}_i)\mathrm{/}{\sim }_U$. Interpret a constant c by the class of $i\mapsto c^{{\mathcal{M}}_i}$, a function symbol F by $([f_1],\dots ,[f_n])\mapsto [i\mapsto F^{{\mathcal{M}}_i}(f_1(i),\dots ,f_n(i))]$, and a relation R by

$R([f_1],\dots ,[f_n])⟺\{i:{\mathcal{M}}_i\models R(f_1(i),\dots ,f_n(i))\}\in U\mathrm{.}$

For zero-arity symbols the tuple is empty. The immediately following quotient lemma verifies equivalence, representative independence and the nonempty carrier. For a constant family write $\mathrm{Ult}(\mathcal{M},U)$, and let $c_a(i)=a$; its diagonal map is $a\mapsto [c_a]$. Elementarity is the subsequent Los theorem, not part of this definition.