let X be TopStruct ; :: thesis: for Y, Z being non empty TopStruct
for f being Function of X,Y
for h being Function of Y,Z st h is being_homeomorphism & f is continuous holds
h * f is continuous
let Y, Z be non empty TopStruct ; :: thesis: for f being Function of X,Y
for h being Function of Y,Z st h is being_homeomorphism & f is continuous holds
h * f is continuous
let f be Function of X,Y; :: thesis: for h being Function of Y,Z st h is being_homeomorphism & f is continuous holds
h * f is continuous
let h be Function of Y,Z; :: thesis: ( h is being_homeomorphism & f is continuous implies h * f is continuous )
assume A1: ( h is being_homeomorphism & f is continuous ) ; :: thesis: h * f is continuous
then h is continuous by TOPS_2:def 5;
hence h * f is continuous by A1, TOPS_2:58; :: thesis: verum