Dass eine Isomorphie elementare Äquivalenz impliziert, wurde in
Fakt
bewiesen. Für die Umkehrung seien also die beiden Strukturen elementar äquivalent, und habe Elemente. Dann gilt in die Aussage
-
und die entsprechende Aussage für gilt nicht. Aufgrund der elementaren Äquivalenz gilt diese Aussage
(bzw. die entsprechende Aussage)
auch
(nicht)
in . D.h. ist ebenfalls endlich mit Elementen.
Wir konstruieren nun sukzessive Teilmengen
,
wobei die
funktional abgeschlossen
sind, und Abbildungen
-
mit
und derart, dass die für jedes Isomorphismen zwischen
und
sind.
Wir wählen
beliebig und setzen als die kleinste, funktional abgeschlossene Teilmenge in an, die enthält. Nach
Fakt
gibt es einen Ausdruck in einer freien Variablen, der die elementare Äquivalenzklasse beschreibt. Wir wählen ein Element
aus der entsprechenden Äquivalenzklasse in
(und diese ist nicht leer wegen der elementaren Äquivalenz zwischen und )
und setzen
-
Für jedes formal-zusammengesetzte Funktionssymbol definieren wir
(hierbei wird überall bzw. eingesetzt)
-
Diese Abbildung ist wohldefiniert. Ist nämlich
-
so gilt in
-
da dies für gilt und daher auch für alle dazu elementar äquivalenten Elemente, und da für die dazu nicht elementar äquivalenten Elemente der Vordersatz nicht gilt. Diese Aussage gilt dann auch bei Interpretation über . Daher ist
-
Wir müssen zeigen, dass ein Homomorphismus vorliegt. Die Verträglichkeit mit den Funktionssymbolen folgt unmittelbar aus der Definition der Abbildung. Ferner wird jedes Element zu einem Element aus der entsprechenden Äquivalenzklasse abgebildet. Nach
(dem Beweis zu)
Fakt
und wegen der elementaren Äquivalenz berücksichtigt daher die Relationen. Dies gilt in beide Richtungen, d.h. eine Relation trifft auf ein Tupel genau dann zu, wenn dies auf das Bildtupel zutrifft. Die Abbildung ist injektiv: Zu zwei Elementen
gibt es zusammengesetzte Funktionssymbole
und
mit
und
Bei
gilt
-
da dies bei Interpretation von durch gilt, und diese Aussage gilt auch in . Die Abbildung ist surjektiv auf das Bild, also liegt wegen der Äquivalenz bei den Relationen insgesamt ein Isomorphismus vor.
Es seien nun und schon konstruiert und
.
Wir wählen
und setzen als die funktionale Hülle von an. Wir betrachten die Menge aller Tupel , wobei
ein Ausdruck in den freien Variablen und ist und wobei
mit der Eigenschaft, dass
-
gilt. Dabei sei eine fixierte Interpretation auf und entsprechend eine Interpretation auf . Es gilt dann insbesondere
-
Daher gilt nach
Fakt
(angewendet auf den Isomorphismus mit
)
auch
-
und insbesondere gibt es ein
(zunächst von abhängiges)
mit
-
Dann gibt es auch ein
,
das man für alle nehmen kann. Für jedes einzelne ist nämlich die erfüllende Elementmenge nicht leer, und wenn der Durchschnitt über alle leer wäre, dann schon für eine endliche Teilmenge und dann auch für die endliche Konjunktion darüber. Es sei ein solches Element. Wir setzen nun
-
und definieren
-
für jedes -stellige formal zusammengesetzte Funktionssymbol . Die Wohldefiniertheit von , die Verträglichkeit mit den Funktionssymbolen und mit den Relationssymbolen
(in beide Richtungen)
sowie die Bijektivität und damit die Isomorphieeigenschaft folgt wie oben.
Da endlich ist, erhalten wir, wenn wir diesen Konstruktionsschritt iterieren, insgesamt eine injektive Abbildung
-
Da
und
gleich viele Elemente besitzen, ist diese auch surjektiv und insgesamt erhalten wir einen Isomorphismus.