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
for y being Point of Y st y = f . x & f is_continuous_at x & g is_continuous_at y 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
for y being Point of Y st y = f . x & f is_continuous_at x & g is_continuous_at y holds
g * f is_continuous_at x
let g be Function of Y,Z; :: thesis: for x being Point of X
for y being Point of Y st y = f . x & f is_continuous_at x & g is_continuous_at y holds
g * f is_continuous_at x
let x be Point of X; :: thesis: for y being Point of Y st y = f . x & f is_continuous_at x & g is_continuous_at y holds
g * f is_continuous_at x
let y be Point of Y; :: thesis: ( y = f . x & f is_continuous_at x & g is_continuous_at y implies g * f is_continuous_at x )
assume A1: y = f . x ; :: thesis: ( not f is_continuous_at x or not g is_continuous_at y or g * f is_continuous_at x )
assume that
A2: f is_continuous_at x and
A3: g is_continuous_at y ; :: thesis: g * f is_continuous_at x
for G being a_neighborhood of (g * f) . x holds (g * f) " G is a_neighborhood of x

proof

let G be a_neighborhood of (g * f) . x; :: thesis: (g * f) " G is a_neighborhood of x
(g * f) . x = g . y by A1, FUNCT_2:15;
then g " G is a_neighborhood of f . x by A1, A3, Th42;
then f " (g " G) is a_neighborhood of x by A2, Th42;
hence (g * f) " G is a_neighborhood of x by RELAT_1:146; :: thesis: verum

end;

hence g * f is_continuous_at x by Th42; :: thesis: verum