let y be Real; :: thesis: for n being Nat
for X being non empty TopSpace
for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds
g is continuous
let n be Nat; :: thesis: for X being non empty TopSpace
for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds
g is continuous
let X be non empty TopSpace; :: thesis: for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds
g is continuous
let f, g be Function of X,(TOP-REAL n); :: thesis: ( f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) implies g is continuous )
assume that
A1: f is continuous and
A2: for p being Point of X holds g . p = y * (f . p) ; :: thesis: g is continuous
for p being Point of X
for V being Subset of (TOP-REAL n) st g . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g .: W c= V )

proof

let p be Point of X; :: thesis: for V being Subset of (TOP-REAL n) st g . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g .: W c= V )
let V be Subset of (TOP-REAL n); :: thesis: ( g . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & g .: W c= V ) )
reconsider r = g . p as Point of (Euclid n) by TOPREAL3:8;
reconsider r1 = f . p as Point of (Euclid n) by TOPREAL3:8;
assume ( g . p in V & V is open ) ; :: thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )
then g . p in Int V by TOPS_1:23;
then consider r0 being Real such that
A3: r0 > 0 and
A4: Ball (r,r0) c= V by GOBOARD6:5;
reconsider G1 = Ball (r1,(r0 / |.y.|)) as Subset of (TOP-REAL n) by TOPREAL3:8;

per cases ( y <> 0 or y = 0 ) ;

suppose A5: y <> 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )

A6: G1 is open by GOBOARD6:3;
A7: 0 < |.y.| by A5, COMPLEX1:47;
then r1 in G1 by A3, GOBOARD6:1, XREAL_1:139;
then consider W1 being Subset of X such that
A8: p in W1 and
A9: W1 is open and
A10: f .: W1 c= G1 by A1, A6, JGRAPH_2:10;
take W1 ; :: thesis: ( p in W1 & W1 is open & g .: W1 c= V )
thus p in W1 by A8; :: thesis: ( W1 is open & g .: W1 c= V )
thus W1 is open by A9; :: thesis: g .: W1 c= V
g .: W1 c= Ball (r,r0)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: W1 or x in Ball (r,r0) )
assume x in g .: W1 ; :: thesis: x in Ball (r,r0)
then consider z being object such that
A11: z in dom g and
A12: z in W1 and
A13: g . z = x by FUNCT_1:def 6;
reconsider z = z as Point of X by A11;
A14: x = y * (f . z) by A2, A13;
then reconsider e1x = x as Point of (Euclid n) by TOPREAL3:8;
reconsider ea1 = f . z as Point of (Euclid n) by TOPREAL3:8;
z in the carrier of X ;
then z in dom f by FUNCT_2:def 1;
then f . z in f .: W1 by A12, FUNCT_1:def 6;
then A15: dist (r1,ea1) < r0 / |.y.| by A10, METRIC_1:11;
r = y * (f . p) by A2;
then dist (r,e1x) < |.y.| * (r0 / |.y.|) by A5, A14, A15, Th13;
then dist (r,e1x) < r0 by A7, XCMPLX_1:87;
hence x in Ball (r,r0) by METRIC_1:11; :: thesis: verum

end;

hence g .: W1 c= V by A4; :: thesis: verum

end;

suppose A16: y = 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )

A17: r = y * (f . p) by A2
.= 0. (TOP-REAL n) by A16, RLVECT_1:10 ;
take W = [#] X; :: thesis: ( p in W & W is open & g .: W c= V )
thus p in W ; :: thesis: ( W is open & g .: W c= V )
thus W is open ; :: thesis: g .: W c= V
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: W or x in V )
assume x in g .: W ; :: thesis: x in V
then consider z being object such that
z in dom g and
A18: z in W and
A19: g . z = x by FUNCT_1:def 6;
reconsider z = z as Point of X by A18;
x = y * (f . z) by A2, A19
.= 0. (TOP-REAL n) by A16, RLVECT_1:10 ;
then x in Ball (r,r0) by A3, A17, GOBOARD6:1;
hence x in V by A4; :: thesis: verum

end;

end;

end;

hence g is continuous by JGRAPH_2:10; :: thesis: verum