set fg = f ^^ g;

set Tn = TOP-REAL n;

set Tm = TOP-REAL m;

set Tnm = TOP-REAL (n + m);

A1: [#] (TOP-REAL n) = the carrier of (TOP-REAL n) ;

A2: TopStruct(# the carrier of (TOP-REAL (n + m)), the topology of (TOP-REAL (n + m)) #) = TopSpaceMetr (Euclid (n + m)) by EUCLID:def 8;

A3: TopStruct(# the carrier of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def 8;

A4: [#] (TOP-REAL m) = the carrier of (TOP-REAL m) ;

A5: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

hence for b_{1} being Function of T,(TOP-REAL (n + m)) st b_{1} = f ^^ g holds

b_{1} is continuous
by A6, TOPS_2:43; :: thesis: verum

set Tn = TOP-REAL n;

set Tm = TOP-REAL m;

set Tnm = TOP-REAL (n + m);

A1: [#] (TOP-REAL n) = the carrier of (TOP-REAL n) ;

A2: TopStruct(# the carrier of (TOP-REAL (n + m)), the topology of (TOP-REAL (n + m)) #) = TopSpaceMetr (Euclid (n + m)) by EUCLID:def 8;

A3: TopStruct(# the carrier of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def 8;

A4: [#] (TOP-REAL m) = the carrier of (TOP-REAL m) ;

A5: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

A6: now :: thesis: for P being Subset of (TOP-REAL (n + m)) st P is open holds

(f ^^ g) " P is open

[#] (TOP-REAL (n + m)) = the carrier of (TOP-REAL (n + m))
;(f ^^ g) " P is open

let P be Subset of (TOP-REAL (n + m)); :: thesis: ( P is open implies (f ^^ g) " P is open )

assume P is open ; :: thesis: (f ^^ g) " P is open

then P in the topology of (TopSpaceMetr (Euclid (n + m))) by A2, PRE_TOPC:def 2;

then reconsider p = P as open Subset of (TopSpaceMetr (Euclid (n + m))) by PRE_TOPC:def 2;

for x being set holds

( x in (f ^^ g) " P iff ex Q being Subset of T st

( Q is open & Q c= (f ^^ g) " P & x in Q ) )

end;assume P is open ; :: thesis: (f ^^ g) " P is open

then P in the topology of (TopSpaceMetr (Euclid (n + m))) by A2, PRE_TOPC:def 2;

then reconsider p = P as open Subset of (TopSpaceMetr (Euclid (n + m))) by PRE_TOPC:def 2;

for x being set holds

( x in (f ^^ g) " P iff ex Q being Subset of T st

( Q is open & Q c= (f ^^ g) " P & x in Q ) )

proof

hence
(f ^^ g) " P is open
by TOPS_1:25; :: thesis: verum
let y be set ; :: thesis: ( y in (f ^^ g) " P iff ex Q being Subset of T st

( Q is open & Q c= (f ^^ g) " P & y in Q ) )

( Q is open & Q c= (f ^^ g) " P & y in Q ) implies y in (f ^^ g) " P ) ; :: thesis: verum

end;( Q is open & Q c= (f ^^ g) " P & y in Q ) )

hereby :: thesis: ( ex Q being Subset of T st

( Q is open & Q c= (f ^^ g) " P & y in Q ) implies y in (f ^^ g) " P )

thus
( ex Q being Subset of T st ( Q is open & Q c= (f ^^ g) " P & y in Q ) implies y in (f ^^ g) " P )

assume A7:
y in (f ^^ g) " P
; :: thesis: ex Q being Element of K10( the carrier of T) st

( Q is open & Q c= (f ^^ g) " P & y in Q )

then A8: y in dom (f ^^ g) by FUNCT_1:def 7;

(f ^^ g) . y in p by A7, FUNCT_1:def 7;

then reconsider e = (f ^^ g) . y as Point of (Euclid (n + m)) by EUCLID:67;

rng e c= REAL ;

then A9: e is FinSequence of REAL by FINSEQ_1:def 4;

A10: dom (f ^^ g) = (dom f) /\ (dom g) by PRE_POLY:def 4;

then A11: y in dom f by A8, XBOOLE_0:def 4;

then f . y in rng f by FUNCT_1:def 3;

then reconsider fy = f . y as Point of (TOP-REAL n) ;

A12: y in dom g by A10, A8, XBOOLE_0:def 4;

then g . y in rng g by FUNCT_1:def 3;

then reconsider gy = g . y as Point of (TOP-REAL m) ;

len e = n + m by CARD_1:def 7;

then consider e1, e2 being FinSequence of REAL such that

A13: len e1 = n and

A14: len e2 = m and

A15: e = e1 ^ e2 by FINSEQ_2:23, A9;

reconsider e2 = e2 as Point of (Euclid m) by TOPREAL7:16, A14;

reconsider e1 = e1 as Point of (Euclid n) by TOPREAL7:16, A13;

A16: fy ^ gy = e1 ^ e2 by PRE_POLY:def 4, A8, A15;

(f ^^ g) . y in p by A7, FUNCT_1:def 7;

then consider r being Real such that

A17: r > 0 and

A18: OpenHypercube (e,r) c= p by Lm1;

OpenHypercube (e2,r) in the topology of (TOP-REAL m) by A3, PRE_TOPC:def 2;

then reconsider O2 = OpenHypercube (e2,r) as open Subset of (TOP-REAL m) by PRE_TOPC:def 2;

A19: g " O2 is open by A4, TOPS_2:43;

OpenHypercube (e1,r) in the topology of (TOP-REAL n) by A5, PRE_TOPC:def 2;

then reconsider O1 = OpenHypercube (e1,r) as open Subset of (TOP-REAL n) by PRE_TOPC:def 2;

take Q = (f " O1) /\ (g " O2); :: thesis: ( Q is open & Q c= (f ^^ g) " P & y in Q )

A20: O2 = product (Intervals (e2,r)) by EUCLID_9:def 4;

f " O1 is open by A1, TOPS_2:43;

hence Q is open by A19; :: thesis: ( Q c= (f ^^ g) " P & y in Q )

A21: OpenHypercube (e,r) = product (Intervals (e,r)) by EUCLID_9:def 4;

len fy = n by CARD_1:def 7;

then dom fy = dom e1 by A13, FINSEQ_3:29;

then A22: fy = (e1 ^ e2) | (dom e1) by FINSEQ_1:21, A16

.= e1 by FINSEQ_1:21 ;

then gy = e2 by A16, FINSEQ_1:33;

then gy in O2 by EUCLID_9:11, A17;

then A23: y in g " O2 by A12, FUNCT_1:def 7;

A24: O1 = product (Intervals (e1,r)) by EUCLID_9:def 4;

thus Q c= (f ^^ g) " P :: thesis: y in Q

then y in f " O1 by A11, FUNCT_1:def 7;

hence y in Q by A23, XBOOLE_0:def 4; :: thesis: verum

end;( Q is open & Q c= (f ^^ g) " P & y in Q )

then A8: y in dom (f ^^ g) by FUNCT_1:def 7;

(f ^^ g) . y in p by A7, FUNCT_1:def 7;

then reconsider e = (f ^^ g) . y as Point of (Euclid (n + m)) by EUCLID:67;

rng e c= REAL ;

then A9: e is FinSequence of REAL by FINSEQ_1:def 4;

A10: dom (f ^^ g) = (dom f) /\ (dom g) by PRE_POLY:def 4;

then A11: y in dom f by A8, XBOOLE_0:def 4;

then f . y in rng f by FUNCT_1:def 3;

then reconsider fy = f . y as Point of (TOP-REAL n) ;

A12: y in dom g by A10, A8, XBOOLE_0:def 4;

then g . y in rng g by FUNCT_1:def 3;

then reconsider gy = g . y as Point of (TOP-REAL m) ;

len e = n + m by CARD_1:def 7;

then consider e1, e2 being FinSequence of REAL such that

A13: len e1 = n and

A14: len e2 = m and

A15: e = e1 ^ e2 by FINSEQ_2:23, A9;

reconsider e2 = e2 as Point of (Euclid m) by TOPREAL7:16, A14;

reconsider e1 = e1 as Point of (Euclid n) by TOPREAL7:16, A13;

A16: fy ^ gy = e1 ^ e2 by PRE_POLY:def 4, A8, A15;

(f ^^ g) . y in p by A7, FUNCT_1:def 7;

then consider r being Real such that

A17: r > 0 and

A18: OpenHypercube (e,r) c= p by Lm1;

OpenHypercube (e2,r) in the topology of (TOP-REAL m) by A3, PRE_TOPC:def 2;

then reconsider O2 = OpenHypercube (e2,r) as open Subset of (TOP-REAL m) by PRE_TOPC:def 2;

A19: g " O2 is open by A4, TOPS_2:43;

OpenHypercube (e1,r) in the topology of (TOP-REAL n) by A5, PRE_TOPC:def 2;

then reconsider O1 = OpenHypercube (e1,r) as open Subset of (TOP-REAL n) by PRE_TOPC:def 2;

take Q = (f " O1) /\ (g " O2); :: thesis: ( Q is open & Q c= (f ^^ g) " P & y in Q )

A20: O2 = product (Intervals (e2,r)) by EUCLID_9:def 4;

f " O1 is open by A1, TOPS_2:43;

hence Q is open by A19; :: thesis: ( Q c= (f ^^ g) " P & y in Q )

A21: OpenHypercube (e,r) = product (Intervals (e,r)) by EUCLID_9:def 4;

len fy = n by CARD_1:def 7;

then dom fy = dom e1 by A13, FINSEQ_3:29;

then A22: fy = (e1 ^ e2) | (dom e1) by FINSEQ_1:21, A16

.= e1 by FINSEQ_1:21 ;

then gy = e2 by A16, FINSEQ_1:33;

then gy in O2 by EUCLID_9:11, A17;

then A23: y in g " O2 by A12, FUNCT_1:def 7;

A24: O1 = product (Intervals (e1,r)) by EUCLID_9:def 4;

thus Q c= (f ^^ g) " P :: thesis: y in Q

proof

fy in O1
by A22, EUCLID_9:11, A17;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in (f ^^ g) " P )

assume A25: x in Q ; :: thesis: x in (f ^^ g) " P

then A26: x in f " O1 by XBOOLE_0:def 4;

then A27: f . x in O1 by FUNCT_1:def 7;

then reconsider fx = f . x as Point of (TOP-REAL n) ;

A28: x in g " O2 by A25, XBOOLE_0:def 4;

then A29: x in dom g by FUNCT_1:def 7;

A30: g . x in O2 by A28, FUNCT_1:def 7;

then reconsider gx = g . x as Point of (TOP-REAL m) ;

A31: fx ^ gx in product ((Intervals (e1,r)) ^ (Intervals (e2,r))) by A24, A20, A27, A30, RLAFFIN3:2;

x in dom f by A26, FUNCT_1:def 7;

then A32: x in dom (f ^^ g) by A29, A10, XBOOLE_0:def 4;

then (f ^^ g) . x = fx ^ gx by PRE_POLY:def 4;

then (f ^^ g) . x in OpenHypercube (e,r) by A31, A15, RLAFFIN3:1, A21;

hence x in (f ^^ g) " P by A18, A32, FUNCT_1:def 7; :: thesis: verum

end;assume A25: x in Q ; :: thesis: x in (f ^^ g) " P

then A26: x in f " O1 by XBOOLE_0:def 4;

then A27: f . x in O1 by FUNCT_1:def 7;

then reconsider fx = f . x as Point of (TOP-REAL n) ;

A28: x in g " O2 by A25, XBOOLE_0:def 4;

then A29: x in dom g by FUNCT_1:def 7;

A30: g . x in O2 by A28, FUNCT_1:def 7;

then reconsider gx = g . x as Point of (TOP-REAL m) ;

A31: fx ^ gx in product ((Intervals (e1,r)) ^ (Intervals (e2,r))) by A24, A20, A27, A30, RLAFFIN3:2;

x in dom f by A26, FUNCT_1:def 7;

then A32: x in dom (f ^^ g) by A29, A10, XBOOLE_0:def 4;

then (f ^^ g) . x = fx ^ gx by PRE_POLY:def 4;

then (f ^^ g) . x in OpenHypercube (e,r) by A31, A15, RLAFFIN3:1, A21;

hence x in (f ^^ g) " P by A18, A32, FUNCT_1:def 7; :: thesis: verum

then y in f " O1 by A11, FUNCT_1:def 7;

hence y in Q by A23, XBOOLE_0:def 4; :: thesis: verum

( Q is open & Q c= (f ^^ g) " P & y in Q ) implies y in (f ^^ g) " P ) ; :: thesis: verum

hence for b

b