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: ( rng f = [#] S & dom g = [#] S ) by A1, A2;
A4: rng g = [#] V by A2;
dom f = [#] T by A1;
hence ( dom (g * f) = [#] T & rng (g * f) = [#] V ) by A3, A4, RELAT_1:27, RELAT_1:28; :: according to TOPS_2:def 5 :: thesis: ( g * f is one-to-one & g * f is continuous & (g * f) " is continuous )
A5: ( f is one-to-one & g is one-to-one ) by A1, A2;
hence g * f is one-to-one ; :: thesis: ( g * f is continuous & (g * f) " is continuous )
( f is continuous & g is continuous ) by A1, A2;
hence g * f is continuous by Th46; :: thesis: (g * f) " is continuous
( f " is continuous & g " is continuous ) by A1, A2;
then (f ") * (g ") is continuous by Th46;
hence (g * f) " is continuous by A3, A4, A5, Th53; :: thesis: verum