let X, Y, Z be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X

for g being Function of Y,Z

for f being Function of X,Y st g is continuous & f | X0 is continuous holds

(g * f) | X0 is continuous

let X0 be non empty SubSpace of X; :: thesis: for g being Function of Y,Z

for f being Function of X,Y st g is continuous & f | X0 is continuous holds

(g * f) | X0 is continuous

let g be Function of Y,Z; :: thesis: for f being Function of X,Y st g is continuous & f | X0 is continuous holds

(g * f) | X0 is continuous

let f be Function of X,Y; :: thesis: ( g is continuous & f | X0 is continuous implies (g * f) | X0 is continuous )

assume A1: ( g is continuous & f | X0 is continuous ) ; :: thesis: (g * f) | X0 is continuous

(g * f) | X0 = g * (f | X0) by Th62;

hence (g * f) | X0 is continuous by A1; :: thesis: verum

for g being Function of Y,Z

for f being Function of X,Y st g is continuous & f | X0 is continuous holds

(g * f) | X0 is continuous

let X0 be non empty SubSpace of X; :: thesis: for g being Function of Y,Z

for f being Function of X,Y st g is continuous & f | X0 is continuous holds

(g * f) | X0 is continuous

let g be Function of Y,Z; :: thesis: for f being Function of X,Y st g is continuous & f | X0 is continuous holds

(g * f) | X0 is continuous

let f be Function of X,Y; :: thesis: ( g is continuous & f | X0 is continuous implies (g * f) | X0 is continuous )

assume A1: ( g is continuous & f | X0 is continuous ) ; :: thesis: (g * f) | X0 is continuous

(g * f) | X0 = g * (f | X0) by Th62;

hence (g * f) | X0 is continuous by A1; :: thesis: verum