set fg = f ^^ g;
set Tn = TOP-REAL n;
set Tm = TOP-REAL m;
set Tnm = TOP-REAL (n + m);
A1: [#] () = the carrier of () ;
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 (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
A4: [#] () = the carrier of () ;
A5: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () 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
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 ;
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
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 ) )

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 )
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 ;
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 ;
then f . y in rng f by FUNCT_1:def 3;
then reconsider fy = f . y as Point of () ;
A12: y in dom g by ;
then g . y in rng g by FUNCT_1:def 3;
then reconsider gy = g . y as Point of () ;
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 ;
reconsider e2 = e2 as Point of () by ;
reconsider e1 = e1 as Point of () by ;
A16: fy ^ gy = e1 ^ e2 by ;
(f ^^ g) . y in p by ;
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 () by ;
then reconsider O2 = OpenHypercube (e2,r) as open Subset of () by PRE_TOPC:def 2;
A19: g " O2 is open by ;
OpenHypercube (e1,r) in the topology of () by ;
then reconsider O1 = OpenHypercube (e1,r) as open Subset of () 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 ;
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 ;
then A22: fy = (e1 ^ e2) | (dom e1) by
.= e1 by FINSEQ_1:21 ;
then gy = e2 by ;
then gy in O2 by ;
then A23: y in g " O2 by ;
A24: O1 = product (Intervals (e1,r)) by EUCLID_9:def 4;
thus Q c= (f ^^ g) " P :: thesis: y in Q
proof
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 () ;
A28: x in g " O2 by ;
then A29: x in dom g by FUNCT_1:def 7;
A30: g . x in O2 by ;
then reconsider gx = g . x as Point of () ;
A31: fx ^ gx in product ((Intervals (e1,r)) ^ (Intervals (e2,r))) by ;
x in dom f by ;
then A32: x in dom (f ^^ g) by ;
then (f ^^ g) . x = fx ^ gx by PRE_POLY:def 4;
then (f ^^ g) . x in OpenHypercube (e,r) by ;
hence x in (f ^^ g) " P by ; :: thesis: verum
end;
fy in O1 by ;
then y in f " O1 by ;
hence y in Q by ; :: thesis: verum
end;
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 ) ; :: thesis: verum
end;
hence (f ^^ g) " P is open by TOPS_1:25; :: thesis: verum
end;
[#] (TOP-REAL (n + m)) = the carrier of (TOP-REAL (n + m)) ;
hence for b1 being Function of T,(TOP-REAL (n + m)) st b1 = f ^^ g holds
b1 is continuous by ; :: thesis: verum