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

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