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 that
A1: h is being_homeomorphism and
A2: f is continuous ; :: thesis: h * f is continuous
h is continuous by A1, TOPS_2:def 5;
hence h * f is continuous by A2, TOPS_2:46; :: thesis: verum