4.1 Vorbereitungen 163
(v) Dom(VERS(⅛*)) =
Dom(VERS(⅛)) и {Dom(^)} и {Dom(^)+1+l | l ∈ Dom(VERS(⅛'))},
(vi) VER(⅛*) = VER(^) и {rα = α1} и VER(⅛') und
(vii) VAN(⅛*) = VAN(^) и {rα = α1} и VAN(⅛,).
Beweis: Durch Induktion uber Dom(>Y) wird gezeigt, dass es unter den entsprechenden
Voraussetzungen immer ein ⅛* gibt, dass (i) bis (v) erfullt. (vi) und (vii) ergeben sich aus
den vorhergehenden Klauseln. Mit (i) bis (v) gilt namlich mit Definition 2-30:
Β ∈ VER(⅛*)
gdw
es gibt ein i ∈ Dom(VERS(⅛*)), so dass Β = A(⅛*i)
gdw
es gibt ein i ∈ Dom(VERS(⅛)) и {Dom(⅛)} и {Dom(⅛)+1+l | l ∈ Dom(VERS(⅛'))}, so
dass Β = A(⅛*i)
gdw
Β ∈ VER(^) и {rα = α1} и VER(⅛').
Sodann ergibt sich (vii) aus (i) bis (v) mit Definition 2-31 wie folgt:
Β ∈ VAN(⅛*)
gdw
es gibt ein i ∈ Dom(VANS(⅛*)), so dass Β = A(⅛*i)
gdw
es gibt ein i ∈ Dom(VERS(⅛*)) ∩ Dom(ANS(⅛*)), so dass Β = A(⅛*i)
gdw
es gibt ein i ∈ (Dom(VERS(⅛)) и {Dom(⅛)} и {Dom(⅛)+1+l | l ∈ Dom(VERS(⅛'))})
∩ Dom(ANS(⅛*)), so dass Β = A(⅛*i)
gdw
es gibt ein i ∈ (Dom(VERS(⅛)) ∩ Dom(ANS(⅛*))) и ({Dom(⅛)} ∩ Dom(ANS(⅛*))) и
({Dom(^)+1+l | l ∈ Dom(VERS(⅛'))} ∩ Dom(ANS(⅛*))), so dass Β = A(^*≈)
gdw
es gibt ein i ∈ (Dom(VERS(⅛)) ∩ Dom(ANS(⅛))) и ({Dom(⅛)} ∩ Dom(ANS(⅛*))) и
({Dom(⅛)+1+l | l ∈ Dom(VERS(⅛'))} ∩ {Dom(⅛)+1+l | l ∈ Dom(ANS⅛'))}), so dass
Β = A(^*i)
gdw
es gibt ein i ∈ Dom(VANS(⅛)) и {Dom(⅛)} и ({Dom(⅛)+1+l | l ∈ Dom(VANS(⅛'))},
so dass Β = A(⅛*i)
gdw
Β ∈ VAN(⅛) и {rα = α1} и VAN(⅛').