D46 Georg Meggle
und
(i.4.2.2) KV(S,H,f,MI(S,H,f,r))
G(S,K(T(S,f) G’(H,I(S,f,G’(H,KV(S,H,f,r)))))
Und daraus dann mit TG1c, C4, TC, C3 und TG1e (i.4.2).
Für (i.4.2.1): Da I(S,f,G’(H,KV(S,H,f,r)) T(S,f) analytisch nach D1,
nach TG1a also auch G’(H,I(S,f,G’(H,KV(S,H,f,r)))) G’(H,T(S,f)), mit
RC, C2 und RG also auch () G(S,K(G’(H,I(S,f,G’(H,KV(S,H,f,r))))
G’(H,T(S,f)))); da G(S,K(G’(H,T(S,f)) T(S,f))) – aus T.V2 – mit ()
wegen TG1c, C4, RC, C2 und TG1e also auch
G(S,K(G’(H,I(S,f,G’(H,KV(S,H,f,r)))) T(S,f)))
Für (i.4.2.2): Wir zeigen:
(i.4.2.2.1) KV(S,H,f,MI(S,H,f,r))
G(S,K(T(S,f) G’(H,I(S,f,G’(H,MI(S,H,f,r)))))
(i.4.2.2.2) KV(S,H,f,MI(S,H,f,r))
G(S,K(T(S,f) G’(H,I(S,f,G’(H,I*( ...