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