let X, Y, Z be non empty TopSpace; :: thesis: for f being Function of X,Y
for g being Function of Y,Z
for x being Point of X st f is_continuous_at x & g is continuous holds
g * f is_continuous_at x
let f be Function of X,Y; :: thesis: for g being Function of Y,Z
for x being Point of X st f is_continuous_at x & g is continuous holds
g * f is_continuous_at x
let g be Function of Y,Z; :: thesis: for x being Point of X st f is_continuous_at x & g is continuous holds
g * f is_continuous_at x
let x be Point of X; :: thesis: ( f is_continuous_at x & g is continuous implies g * f is_continuous_at x )
assume A1: f is_continuous_at x ; :: thesis: ( not g is continuous or g * f is_continuous_at x )
assume g is continuous ; :: thesis: g * f is_continuous_at x
then g is_continuous_at f . x ;
hence g * f is_continuous_at x by A1, Th47; :: thesis: verum