let X, Y, Z be non empty TopSpace; :: thesis: for f being Function of X,Y
for g being Function of Y,Z
for y being Point of Y st f is continuous & g is_continuous_at y holds
for x being Point of X st x in f " {y} holds
g * f is_continuous_at x
let f be Function of X,Y; :: thesis: for g being Function of Y,Z
for y being Point of Y st f is continuous & g is_continuous_at y holds
for x being Point of X st x in f " {y} holds
g * f is_continuous_at x
let g be Function of Y,Z; :: thesis: for y being Point of Y st f is continuous & g is_continuous_at y holds
for x being Point of X st x in f " {y} holds
g * f is_continuous_at x
let y be Point of Y; :: thesis: ( f is continuous & g is_continuous_at y implies for x being Point of X st x in f " {y} holds
g * f is_continuous_at x )
assume A1: f is continuous ; :: thesis: ( not g is_continuous_at y or for x being Point of X st x in f " {y} holds
g * f is_continuous_at x )
assume A2: g is_continuous_at y ; :: thesis: for x being Point of X st x in f " {y} holds
g * f is_continuous_at x
let x be Point of X; :: thesis: ( x in f " {y} implies g * f is_continuous_at x )
assume x in f " {y} ; :: thesis: g * f is_continuous_at x
then {x} is Subset of (f " {y}) by SUBSET_1:41;
then ( dom f = [#] X & Im (f,x) c= {y} ) by FUNCT_2:95, FUNCT_2:def 1;
then A3: {(f . x)} c= {y} by FUNCT_1:59;
f . x in {(f . x)} by TARSKI:def 1;
then A4: f . x = y by A3, TARSKI:def 1;
f is_continuous_at x by A1;
hence g * f is_continuous_at x by A2, A4, Th47; :: thesis: verum