Wir wollen zeigen, dass im Sequenzenkalkül
-
ableitbar ist, was inhaltlich bedeutet, dass die Hintereinanderschaltung von zwei surjektiven Abbildungen wieder surjektiv ist. Es sei dazu die Vereinigung der beiden Vordersätze. Wir haben dann
-
zu zeigen. Wir zeigen zunächst die entsprechende Existenzaussage. Aufgrund der Substitution gilt
-
Daraus folgt durch zweimalige Existenzaussage
-
Da rechts gar nicht vorkommt, erhält man aus
-
durch Existenzeinführung im Antezedens
-
Aufgrund der Existeneinführung im Sukzedens gilt
-
und
-
Durch Vertauschen der Existenzoperatoren und die Transititvität der Implikation erhält man
-
-
Wir haben zunächst
-
und
-
also
-
Ebenso erhält man
-
Es gilt ferner (Substitutionsregel)
-
was wir als
-
schreiben.