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

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

hence
g * f is_continuous_at x
by Th42; :: thesis: verum
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;(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