let Z, Y, X 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 A3: x in f " {y} ; :: thesis: g * f is_continuous_at x
A4: dom f = [#] X by FUNCT_2:def 1;
{x} is Subset of (f " {y}) by A3, SUBSET_1:63;
then Im f,x c= {y} by FUNCT_2:172;
then ( {(f . x)} c= {y} & f . x in {(f . x)} ) by A4, FUNCT_1:117, TARSKI:def 1;
then ( f is_continuous_at x & f . x = y ) by A1, Th49, TARSKI:def 1;
hence g * f is_continuous_at x by A2, Th52; :: thesis: verum