let X be TopStruct ; 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 ; 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; 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; ( h is being_homeomorphism & f is continuous implies h * f is continuous )
assume that
A1:
h is being_homeomorphism
and
A2:
f is continuous
; h * f is continuous
h is continuous
by A1, TOPS_2:def 5;
hence
h * f is continuous
by A2, TOPS_2:46; verum