let x, y be Real; :: thesis: for n being Nat
for X being non empty TopSpace
for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds
g is continuous
let n be Nat; :: thesis: for X being non empty TopSpace
for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds
g is continuous
let X be non empty TopSpace; :: thesis: for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds
g is continuous
let f1, f2, g be Function of X,(TOP-REAL n); :: thesis: ( f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) implies g is continuous )
assume that
A1: f1 is continuous and
A2: f2 is continuous and
A3: for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ; :: thesis: g is continuous

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

suppose that A4: x <> 0 and
A5: y <> 0 ; :: 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;
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
A6: r0 > 0 and
A7: Ball (r,r0) c= V by GOBOARD6:5;
A8: r0 / 2 > 0 by A6, XREAL_1:215;
reconsider r2 = f2 . p as Point of (Euclid n) by TOPREAL3:8;
reconsider G2 = Ball (r2,((r0 / 2) / |.y.|)) as Subset of (TOP-REAL n) by TOPREAL3:8;
A9: G2 is open by GOBOARD6:3;
reconsider r1 = f1 . p as Point of (Euclid n) by TOPREAL3:8;
reconsider G1 = Ball (r1,((r0 / 2) / |.x.|)) as Subset of (TOP-REAL n) by TOPREAL3:8;
A10: G1 is open by GOBOARD6:3;
A11: |.y.| > 0 by A5, COMPLEX1:47;
then r2 in G2 by A8, GOBOARD6:1, XREAL_1:139;
then consider W2 being Subset of X such that
A12: p in W2 and
A13: W2 is open and
A14: f2 .: W2 c= G2 by A2, A9, JGRAPH_2:10;
A15: |.x.| > 0 by A4, COMPLEX1:47;
then r1 in G1 by A8, GOBOARD6:1, XREAL_1:139;
then consider W1 being Subset of X such that
A16: p in W1 and
A17: W1 is open and
A18: f1 .: W1 c= G1 by A1, A10, JGRAPH_2:10;
take W = W1 /\ W2; :: thesis: ( p in W & W is open & g .: W c= V )
thus p in W by A16, A12, XBOOLE_0:def 4; :: thesis: ( W is open & g .: W c= V )
thus W is open by A17, A13; :: thesis: g .: W c= V
g .: W c= Ball (r,r0)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in g .: W or a in Ball (r,r0) )
assume a in g .: W ; :: thesis: a in Ball (r,r0)
then consider z being object such that
A19: z in dom g and
A20: z in W and
A21: g . z = a by FUNCT_1:def 6;
A22: z in W1 by A20, XBOOLE_0:def 4;
reconsider z = z as Point of X by A19;
reconsider ea2 = f2 . z as Point of (Euclid n) by TOPREAL3:8;
reconsider ea1 = f1 . z as Point of (Euclid n) by TOPREAL3:8;
A23: z in the carrier of X ;
then A24: z in dom f2 by FUNCT_2:def 1;
z in W2 by A20, XBOOLE_0:def 4;
then f2 . z in f2 .: W2 by A24, FUNCT_1:def 6;
then A25: dist (r2,ea2) < (r0 / 2) / |.y.| by A14, METRIC_1:11;
z in dom f1 by A23, FUNCT_2:def 1;
then f1 . z in f1 .: W1 by A22, FUNCT_1:def 6;
then A26: dist (r1,ea1) < (r0 / 2) / |.x.| by A18, METRIC_1:11;
A27: a = (x * (f1 . z)) + (y * (f2 . z)) by A3, A21;
then reconsider e1x = a as Point of (Euclid n) by TOPREAL3:8;
r = (x * (f1 . p)) + (y * (f2 . p)) by A3;
then dist (r,e1x) < (|.x.| * ((r0 / 2) / |.x.|)) + (|.y.| * ((r0 / 2) / |.y.|)) by A4, A5, A27, A26, A25, Th14;
then dist (r,e1x) < (|.x.| * ((r0 / |.x.|) / 2)) + (|.y.| * ((r0 / 2) / |.y.|)) by XCMPLX_1:48;
then dist (r,e1x) < (|.x.| * ((r0 / |.x.|) / 2)) + (|.y.| * ((r0 / |.y.|) / 2)) by XCMPLX_1:48;
then dist (r,e1x) < (r0 / 2) + (|.y.| * ((r0 / |.y.|) / 2)) by A15, XCMPLX_1:97;
then dist (r,e1x) < (r0 / 2) + (r0 / 2) by A11, XCMPLX_1:97;
hence a in Ball (r,r0) by METRIC_1:11; :: thesis: verum

end;

hence g .: W c= V by A7; :: thesis: verum

end;

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

end;

suppose A28: x = 0 ; :: thesis: g is continuous

for p being Point of X holds g . p = y * (f2 . p)

proof

let p be Point of X; :: thesis: g . p = y * (f2 . p)
thus g . p = (x * (f1 . p)) + (y * (f2 . p)) by A3
.= (0. (TOP-REAL n)) + (y * (f2 . p)) by A28, RLVECT_1:10
.= y * (f2 . p) by RLVECT_1:4 ; :: thesis: verum

end;

hence g is continuous by A2, Th15; :: thesis: verum

end;

suppose A29: y = 0 ; :: thesis: g is continuous

for p being Point of X holds g . p = x * (f1 . p)

proof

let p be Point of X; :: thesis: g . p = x * (f1 . p)
thus g . p = (x * (f1 . p)) + (y * (f2 . p)) by A3
.= (x * (f1 . p)) + (0. (TOP-REAL n)) by A29, RLVECT_1:10
.= x * (f1 . p) by RLVECT_1:4 ; :: thesis: verum

end;

hence g is continuous by A1, Th15; :: thesis: verum

end;

end;