let y be real number ; :: 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:13;
A3: n in NAT by ORDINAL1:def 13;
reconsider r1 = f . p as Point of (Euclid n) by TOPREAL3:13;
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:55;
then consider r0 being real number such that
A4: r0 > 0 and
A5: Ball (r,r0) c= V by A3, GOBOARD6:8;
reconsider G1 = Ball (r1,(r0 / (abs y))) as Subset of (TOP-REAL n) by TOPREAL3:13;

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

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

A7: G1 is open by A3, GOBOARD6:6;
A8: 0 < abs y by A6, COMPLEX1:133;
then r1 in G1 by A4, GOBOARD6:4, XREAL_1:141;
then consider W1 being Subset of X such that
A9: p in W1 and
A10: W1 is open and
A11: f .: W1 c= G1 by A1, A7, JGRAPH_2:20;
take W1 ; :: thesis: ( p in W1 & W1 is open & g .: W1 c= V )
thus p in W1 by A9; :: thesis: ( W1 is open & g .: W1 c= V )
thus W1 is open by A10; :: thesis: g .: W1 c= V
g .: W1 c= Ball (r,r0)

proof

let x be set ; :: 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 set such that
A12: z in dom g and
A13: z in W1 and
A14: g . z = x by FUNCT_1:def 12;
reconsider z = z as Point of X by A12;
A15: x = y * (f . z) by A2, A14;
then reconsider e1x = x as Point of (Euclid n) by TOPREAL3:13;
reconsider ea1 = f . z as Point of (Euclid n) by TOPREAL3:13;
z in the carrier of X ;
then z in dom f by FUNCT_2:def 1;
then f . z in f .: W1 by A13, FUNCT_1:def 12;
then A16: dist (r1,ea1) < r0 / (abs y) by A11, METRIC_1:12;
r = y * (f . p) by A2;
then dist (r,e1x) < (abs y) * (r0 / (abs y)) by A6, A15, A16, Th13;
then dist (r,e1x) < r0 by A8, XCMPLX_1:88;
hence x in Ball (r,r0) by METRIC_1:12; :: thesis: verum

end;

hence g .: W1 c= V by A5, XBOOLE_1:1; :: thesis: verum

end;

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

A18: r = y * (f . p) by A2
.= 0. (TOP-REAL n) by A17, EUCLID:33 ;
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 set ; :: 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 set such that
z in dom g and
A19: z in W and
A20: g . z = x by FUNCT_1:def 12;
reconsider z = z as Point of X by A19;
x = y * (f . z) by A2, A20
.= 0. (TOP-REAL n) by A17, EUCLID:33 ;
then x in Ball (r,r0) by A4, A18, GOBOARD6:4;
hence x in V by A5; :: thesis: verum

end;

end;

end;

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