Beweise D89
und
(ii) GG(P,sXY(s XP(s) YP(s)
(T(X,f) G(X,KV(X,Y,f,r)))) B(P,,f,r)
Für (i): Aus B(P,,f,r) wie im Beweis für T.B2.2 (ii) bereits gezeigt:
sXY(s S(X,s) H(Y,s) (G(X,T(X,f)) G(X,KV(S,H,f,r)))).
Daraus aber mit P1 sXY(s S(X,s) H(Y,s) X=a (T(X,f))
G(X,KV(S,H,f,r)))) (*). Daraus B(P,,f,r). Nun aber nach T.B2.1 GG(P,
B(P,,f,r)), wegen T.G0 und T.G1 also auch GG(P,sXY(s S(X,s)
H(Y,s) X=a (T(X,f)) G(X,KV(S,H,f,r)))).
Für (ii): Aus (*) GG(P,sXY(s S(X,s) H(Y,s) (T(X,f)
G(X,KV(X,Y,f,r)))) analog wie in Beweis für T.B2.2. sXY(s S(X,s)
H(Y,s) (T(X,f) G(X,KV(X,Y,f,r))), welches nach T.K44 äquivalent
mit sXY(s S(X,s)