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;
A6:
now 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));
( P is open implies (f ^^ g) " P is open )assume
P is
open
;
(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
let y be
set ;
( 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 ( 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
;
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);
( 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;
( 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
y in Qproof
let x be
object ;
TARSKI:def 3 ( not x in Q or x in (f ^^ g) " P )
assume A25:
x in Q
;
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;
verum
end;
fy in O1
by A22, EUCLID_9:11, A17;
then
y in f " O1
by A11, FUNCT_1:def 7;
hence
y in Q
by A23, XBOOLE_0:def 4;
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 )
;
verum
end; hence
(f ^^ g) " P is
open
by TOPS_1:25;
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 A6, TOPS_2:43; verum