let T, S, V be non empty TopStruct ; :: thesis: for f being Function of T,S
for g being Function of S,V st f is being_homeomorphism & g is being_homeomorphism holds
g * f is being_homeomorphism
let f be Function of T,S; :: thesis: for g being Function of S,V st f is being_homeomorphism & g is being_homeomorphism holds
g * f is being_homeomorphism
let g be Function of S,V; :: thesis: ( f is being_homeomorphism & g is being_homeomorphism implies g * f is being_homeomorphism )
assume that
A1: f is being_homeomorphism and
A2: g is being_homeomorphism ; :: thesis: g * f is being_homeomorphism
A3: ( dom f = [#] T & rng f = [#] S & f is one-to-one & f is continuous & f " is continuous ) by A1, Def5;
A4: ( dom g = [#] S & rng g = [#] V & g is one-to-one & g is continuous & g " is continuous ) by A2, Def5;
hence ( dom (g * f) = [#] T & rng (g * f) = [#] V ) by A3, RELAT_1:46, RELAT_1:47; :: according to TOPS_2:def 5 :: thesis: ( g * f is one-to-one & g * f is continuous & (g * f) " is continuous )
thus g * f is one-to-one by A3, A4, FUNCT_1:46; :: thesis: ( g * f is continuous & (g * f) " is continuous )
thus g * f is continuous by A3, A4, Th58; :: thesis: (g * f) " is continuous
(f " ) * (g " ) is continuous by A3, A4, Th58;
hence (g * f) " is continuous by A3, A4, Th66; :: thesis: verum