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

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