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

proof

let a be set ; :: 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 set such that
A20: z in dom g and
A21: z in W and
A22: g . z = a by FUNCT_1:def 6;
A23: z in W1 by A21, XBOOLE_0:def 4;
reconsider z = z as Point of X by A20;
reconsider ea2 = f2 . z as Point of (Euclid n) by TOPREAL3:8;
reconsider ea1 = f1 . z as Point of (Euclid n) by TOPREAL3:8;
A24: z in the carrier of X ;
then A25: z in dom f2 by FUNCT_2:def 1;
z in W2 by A21, XBOOLE_0:def 4;
then f2 . z in f2 .: W2 by A25, FUNCT_1:def 6;
then A26: dist (r2,ea2) < (r0 / 2) / (abs y) by A15, METRIC_1:11;
z in dom f1 by A24, FUNCT_2:def 1;
then f1 . z in f1 .: W1 by A23, FUNCT_1:def 6;
then A27: dist (r1,ea1) < (r0 / 2) / (abs x) by A19, METRIC_1:11;
A28: a = (x * (f1 . z)) + (y * (f2 . z)) by A3, A22;
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) < ((abs x) * ((r0 / 2) / (abs x))) + ((abs y) * ((r0 / 2) / (abs y))) by A4, A5, A28, A27, A26, Th14;
then dist (r,e1x) < ((abs x) * ((r0 / (abs x)) / 2)) + ((abs y) * ((r0 / 2) / (abs y))) by XCMPLX_1:48;
then dist (r,e1x) < ((abs x) * ((r0 / (abs x)) / 2)) + ((abs y) * ((r0 / (abs y)) / 2)) by XCMPLX_1:48;
then dist (r,e1x) < (r0 / 2) + ((abs y) * ((r0 / (abs y)) / 2)) by A16, XCMPLX_1:97;
then dist (r,e1x) < (r0 / 2) + (r0 / 2) by A12, XCMPLX_1:97;
hence a in Ball (r,r0) by METRIC_1:11; :: thesis: verum

end;

hence g .: W c= V by A8, XBOOLE_1:1; :: thesis: verum

end;

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

end;

suppose A29: 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 A29, EUCLID:29
.= y * (f2 . p) by EUCLID:27 ; :: thesis: verum

end;

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

end;

suppose A30: 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 A30, EUCLID:29
.= x * (f1 . p) by EUCLID:27 ; :: thesis: verum

end;

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

end;

end;