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