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