let X, Y, Z be non empty TopSpace; 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; 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; 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; ( 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
; ( 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
; for x being Point of X st x in f " {y} holds
g * f is_continuous_at x
let x be Point of X; ( x in f " {y} implies g * f is_continuous_at x )
assume
x in f " {y}
; 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; verum