A principal ultrapower is the original structure

In the displayed U, a coordinate equality set belongs to U exactly when f(i_0)=g(i_0). This proves directly that the quotient equivalence is equality at i_0 and evaluation is well-defined and injective. Every a in M has the explicitly defined constant function c_a in the product, so evaluation is surjective and sends [c_a] to a. Nonemptiness of M therefore gives a nonempty product and quotient, without any family of choices.

A constant symbol evaluates at i_0 to its original interpretation. For a function symbol F and representatives f_1,...,f_n, evaluation of its interpreted class is exactly $F^M(f_1(i_0),\dots ,f_n(i_0))$. This also shows independence of representatives in that interpreted symbol. A relation holds in the quotient exactly when its coordinate truth set contains i_0, that is, when it holds on the evaluated tuple in M. Thus evaluation preserves functions and preserves and reflects relations, including equality by step 1.1; it is an isomorphism. Zero-arity symbols give the same calculation with the empty tuple. This local verification uses the formulas of F1, not the choice-dependent general Los theorem.