let i, j be Element of NAT ; ex f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) st
( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj ) )
set ci = the carrier of (Euclid i);
set cj = the carrier of (Euclid j);
set cij = the carrier of (Euclid (i + j));
defpred S1[ Element of the carrier of (Euclid i), Element of the carrier of (Euclid j), set ] means ex fi, fj being FinSequence of REAL st
( fi = $1 & fj = $2 & $3 = fi ^ fj );
A1:
the carrier of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) = the carrier of (max-Prod2 ((Euclid i),(Euclid j)))
by TOPMETR:12;
A2:
for x being Element of the carrier of (Euclid i)
for y being Element of the carrier of (Euclid j) ex u being Element of the carrier of (Euclid (i + j)) st S1[x,y,u]
proof
let x be
Element of the
carrier of
(Euclid i);
for y being Element of the carrier of (Euclid j) ex u being Element of the carrier of (Euclid (i + j)) st S1[x,y,u]let y be
Element of the
carrier of
(Euclid j);
ex u being Element of the carrier of (Euclid (i + j)) st S1[x,y,u]
(
x is
Element of
REAL i &
y is
Element of
REAL j )
;
then reconsider fi =
x,
fj =
y as
FinSequence of
REAL ;
fi ^ fj is
Tuple of
i + j,
REAL
by FINSEQ_2:107;
then reconsider u =
fi ^ fj as
Element of the
carrier of
(Euclid (i + j)) by FINSEQ_2:131;
take
u
;
S1[x,y,u]
thus
S1[
x,
y,
u]
;
verum
end;
consider f being Function of [: the carrier of (Euclid i), the carrier of (Euclid j):], the carrier of (Euclid (i + j)) such that
A3:
for x being Element of the carrier of (Euclid i)
for y being Element of the carrier of (Euclid j) holds S1[x,y,f . (x,y)]
from BINOP_1:sch 3(A2);
A4:
[: the carrier of (Euclid i), the carrier of (Euclid j):] = the carrier of (max-Prod2 ((Euclid i),(Euclid j)))
by Def1;
the carrier of (TopSpaceMetr (Euclid (i + j))) = the carrier of (Euclid (i + j))
by TOPMETR:12;
then reconsider f = f as Function of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))),(TopSpaceMetr (Euclid (i + j))) by A4, A1;
A5:
[:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] = TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))
by Th23;
then reconsider f = f as Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) ;
take
f
; ( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj ) )
thus
dom f = [#] [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]
by FUNCT_2:def 1; TOPS_2:def 5 ( rng f = [#] (TopSpaceMetr (Euclid (i + j))) & f is one-to-one & f is continuous & f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj ) )
thus A6:
rng f = [#] (TopSpaceMetr (Euclid (i + j)))
( f is one-to-one & f is continuous & f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj ) )proof
thus
rng f c= [#] (TopSpaceMetr (Euclid (i + j)))
;
XBOOLE_0:def 10 [#] (TopSpaceMetr (Euclid (i + j))) c= rng f
let y be
object ;
TARSKI:def 3 ( not y in [#] (TopSpaceMetr (Euclid (i + j))) or y in rng f )
assume
y in [#] (TopSpaceMetr (Euclid (i + j)))
;
y in rng f
then reconsider k =
y as
Element of
REAL (i + j) by TOPMETR:12;
len k = i + j
by CARD_1:def 7;
then consider g,
h being
FinSequence of
REAL such that A7:
(
len g = i &
len h = j )
and A8:
k = g ^ h
by FINSEQ_2:23;
A9:
(
g in the
carrier of
(Euclid i) &
h in the
carrier of
(Euclid j) )
by A7, Th16;
then
[g,h] in [: the carrier of (Euclid i), the carrier of (Euclid j):]
by ZFMISC_1:87;
then A10:
[g,h] in dom f
by FUNCT_2:def 1;
ex
fi,
fj being
FinSequence of
REAL st
(
fi = g &
fj = h &
f . (
g,
h)
= fi ^ fj )
by A3, A9;
hence
y in rng f
by A8, A10, FUNCT_1:def 3;
verum
end;
thus A11:
f is one-to-one
( f is continuous & f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj ) )proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume
x1 in dom f
;
( not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
then consider x1a,
x1b being
object such that A12:
x1a in the
carrier of
(Euclid i)
and A13:
x1b in the
carrier of
(Euclid j)
and A14:
x1 = [x1a,x1b]
by A4, A1, A5, ZFMISC_1:def 2;
assume
x2 in dom f
;
( not f . x1 = f . x2 or x1 = x2 )
then consider x2a,
x2b being
object such that A15:
x2a in the
carrier of
(Euclid i)
and A16:
x2b in the
carrier of
(Euclid j)
and A17:
x2 = [x2a,x2b]
by A4, A1, A5, ZFMISC_1:def 2;
assume A18:
f . x1 = f . x2
;
x1 = x2
consider fi1,
fj1 being
FinSequence of
REAL such that A19:
fi1 = x1a
and A20:
fj1 = x1b
and A21:
f . (
x1a,
x1b)
= fi1 ^ fj1
by A3, A12, A13;
consider fi2,
fj2 being
FinSequence of
REAL such that A22:
fi2 = x2a
and A23:
fj2 = x2b
and A24:
f . (
x2a,
x2b)
= fi2 ^ fj2
by A3, A15, A16;
len fj1 = j
by A13, A20, CARD_1:def 7;
then A25:
len fj1 = len fj2
by A16, A23, CARD_1:def 7;
A26:
len fi1 = i
by A12, A19, CARD_1:def 7;
then
len fi1 = len fi2
by A15, A22, CARD_1:def 7;
then
fi1 = fi2
by A14, A17, A21, A24, A25, A18, Th5;
hence
x1 = x2
by A14, A17, A19, A20, A21, A22, A23, A24, A26, A25, A18, Th5;
verum
end;
A27:
for P being Subset of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) st P is open holds
(f ") " P is open
proof
let P be
Subset of
(TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j))));
( P is open implies (f ") " P is open )
assume
P is
open
;
(f ") " P is open
then
P in the
topology of
(TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j))))
;
then A28:
P in Family_open_set (max-Prod2 ((Euclid i),(Euclid j)))
by TOPMETR:12;
A29:
for
x being
Point of
(Euclid (i + j)) st
x in f .: P holds
ex
r being
Real st
(
r > 0 &
Ball (
x,
r)
c= f .: P )
proof
let x be
Point of
(Euclid (i + j));
( x in f .: P implies ex r being Real st
( r > 0 & Ball (x,r) c= f .: P ) )
assume
x in f .: P
;
ex r being Real st
( r > 0 & Ball (x,r) c= f .: P )
then consider a being
object such that A30:
a in the
carrier of
(TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j))))
and A31:
a in P
and A32:
x = f . a
by FUNCT_2:64;
reconsider a =
a as
Point of
(max-Prod2 ((Euclid i),(Euclid j))) by A30, TOPMETR:12;
consider r being
Real such that A33:
r > 0
and A34:
Ball (
a,
r)
c= P
by A28, A31, PCOMPS_1:def 4;
take
r
;
( r > 0 & Ball (x,r) c= f .: P )
thus
r > 0
by A33;
Ball (x,r) c= f .: P
let b be
object ;
TARSKI:def 3 ( not b in Ball (x,r) or b in f .: P )
assume A35:
b in Ball (
x,
r)
;
b in f .: P
then reconsider bb =
b as
Point of
(Euclid (i + j)) ;
reconsider bb2 =
bb,
xx2 =
x as
Element of
REAL (i + j) ;
dist (
bb,
x)
< r
by A35, METRIC_1:11;
then
|.(bb2 - xx2).| < r
by EUCLID:def 6;
then A36:
sqrt (Sum (sqr (abs (bb2 - xx2)))) < r
by EUCLID:25;
reconsider k =
bb as
Element of
REAL (i + j) ;
len k = i + j
by CARD_1:def 7;
then consider g,
h being
FinSequence of
REAL such that A37:
len g = i
and A38:
len h = j
and A39:
k = g ^ h
by FINSEQ_2:23;
reconsider hh =
h as
Point of
(Euclid j) by A38, Th16;
reconsider gg =
g as
Point of
(Euclid i) by A37, Th16;
consider g,
h being
FinSequence of
REAL such that A40:
g = gg
and A41:
h = hh
and A42:
f . (
gg,
hh)
= g ^ h
by A3;
reconsider gg2 =
gg,
a12 =
a `1 as
Element of
REAL i ;
A43:
(
max (
(dist (gg,(a `1))),
(dist (hh,(a `2))))
= dist (
gg,
(a `1)) or
max (
(dist (gg,(a `1))),
(dist (hh,(a `2))))
= dist (
hh,
(a `2)) )
by XXREAL_0:16;
consider p,
q being
object such that A44:
p in the
carrier of
(Euclid i)
and A45:
q in the
carrier of
(Euclid j)
and A46:
a = [p,q]
by A4, ZFMISC_1:def 2;
reconsider q =
q as
Element of the
carrier of
(Euclid j) by A45;
reconsider p =
p as
Element of the
carrier of
(Euclid i) by A44;
consider fi,
fj being
FinSequence of
REAL such that A47:
fi = p
and A48:
fj = q
and A49:
f . (
p,
q)
= fi ^ fj
by A3;
A50:
(
len fi = i &
len fj = j )
by A47, A48, CARD_1:def 7;
(
len g = i &
len h = j )
by A40, A41, CARD_1:def 7;
then
sqrt (Sum (sqr ((abs (g - fi)) ^ (abs (h - fj))))) < r
by A32, A39, A46, A49, A40, A41, A50, A36, Th15;
then
sqrt (Sum ((sqr (abs (g - fi))) ^ (sqr (abs (h - fj))))) < r
by Th10;
then A51:
sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj))))) < r
by RVSUM_1:75;
reconsider hh2 =
hh,
a22 =
a `2 as
Element of
REAL j ;
A52:
a22 = q
by A46;
0 <= Sum (sqr (abs (g - fi)))
by RVSUM_1:86;
then
(
0 <= Sum (sqr (abs (hh2 - a22))) &
(Sum (sqr (abs (hh2 - a22)))) + 0 <= (Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))) )
by A48, A41, A52, RVSUM_1:86, XREAL_1:7;
then
sqrt (Sum (sqr (abs (hh2 - a22)))) <= sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))))
by SQUARE_1:26;
then
sqrt (Sum (sqr (abs (hh2 - a22)))) < r
by A51, XXREAL_0:2;
then
|.(hh2 - a22).| < r
by EUCLID:25;
then A53:
(Pitag_dist j) . (
hh2,
a22)
< r
by EUCLID:def 6;
A54:
a12 = p
by A46;
0 <= Sum (sqr (abs (h - fj)))
by RVSUM_1:86;
then
(
0 <= Sum (sqr (abs (gg2 - a12))) &
(Sum (sqr (abs (gg2 - a12)))) + 0 <= (Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))) )
by A47, A40, A54, RVSUM_1:86, XREAL_1:7;
then
sqrt (Sum (sqr (abs (gg2 - a12)))) <= sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))))
by SQUARE_1:26;
then
sqrt (Sum (sqr (abs (gg2 - a12)))) < r
by A51, XXREAL_0:2;
then
|.(gg2 - a12).| < r
by EUCLID:25;
then A55:
(Pitag_dist i) . (
gg2,
a12)
< r
by EUCLID:def 6;
dist (
[gg,hh],
[(a `1),(a `2)])
= max (
(dist (gg,(a `1))),
(dist (hh,(a `2))))
by Th18;
then
dist (
[gg,hh],
a)
< r
by A4, A55, A53, A43, MCART_1:21;
then
[g,h] in Ball (
a,
r)
by A40, A41, METRIC_1:11;
then
[g,h] in P
by A34;
hence
b in f .: P
by A39, A40, A41, A42, FUNCT_2:35;
verum
end;
f .: P is
Subset of
(Euclid (i + j))
by TOPMETR:12;
then
f .: P in Family_open_set (Euclid (i + j))
by A29, PCOMPS_1:def 4;
then
f .: P in the
topology of
(TopSpaceMetr (Euclid (i + j)))
by TOPMETR:12;
hence
(f ") " P in the
topology of
(TopSpaceMetr (Euclid (i + j)))
by A6, A11, A5, TOPS_2:54;
PRE_TOPC:def 2 verum
end;
A56:
for P being Subset of (TopSpaceMetr (Euclid (i + j))) st P is open holds
f " P is open
proof
let P be
Subset of
(TopSpaceMetr (Euclid (i + j)));
( P is open implies f " P is open )
assume
P is
open
;
f " P is open
then
P in the
topology of
(TopSpaceMetr (Euclid (i + j)))
;
then A57:
P in Family_open_set (Euclid (i + j))
by TOPMETR:12;
A58:
for
x being
Point of
(max-Prod2 ((Euclid i),(Euclid j))) st
x in f " P holds
ex
r being
Real st
(
r > 0 &
Ball (
x,
r)
c= f " P )
proof
let x be
Point of
(max-Prod2 ((Euclid i),(Euclid j)));
( x in f " P implies ex r being Real st
( r > 0 & Ball (x,r) c= f " P ) )
assume A59:
x in f " P
;
ex r being Real st
( r > 0 & Ball (x,r) c= f " P )
then
f . x in the
carrier of
(TopSpaceMetr (Euclid (i + j)))
by FUNCT_2:5;
then reconsider fx =
f . x as
Point of
(Euclid (i + j)) by TOPMETR:12;
f . x in P
by A59, FUNCT_2:38;
then consider r being
Real such that A60:
r > 0
and A61:
Ball (
fx,
r)
c= P
by A57, PCOMPS_1:def 4;
take r1 =
r / 2;
( r1 > 0 & Ball (x,r1) c= f " P )
thus
r1 > 0
by A60, XREAL_1:139;
Ball (x,r1) c= f " P
let b be
object ;
TARSKI:def 3 ( not b in Ball (x,r1) or b in f " P )
assume A62:
b in Ball (
x,
r1)
;
b in f " P
then reconsider bb =
b as
Point of
(max-Prod2 ((Euclid i),(Euclid j))) ;
A63:
dist (
bb,
x)
< r1
by A62, METRIC_1:11;
bb in the
carrier of
(max-Prod2 ((Euclid i),(Euclid j)))
;
then A64:
bb in the
carrier of
(TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j))))
by TOPMETR:12;
then
f . bb in the
carrier of
(TopSpaceMetr (Euclid (i + j)))
by FUNCT_2:5;
then reconsider fb =
f . b as
Point of
(Euclid (i + j)) by TOPMETR:12;
reconsider fbb =
fb,
fxx =
fx as
Element of
REAL (i + j) ;
consider b1,
x1 being
Point of
(Euclid i),
b2,
x2 being
Point of
(Euclid j) such that A65:
(
bb = [b1,b2] &
x = [x1,x2] )
and
the
distance of
(max-Prod2 ((Euclid i),(Euclid j))) . (
bb,
x)
= max (
( the distance of (Euclid i) . (b1,x1)),
( the distance of (Euclid j) . (b2,x2)))
by Def1;
A66:
dist (
[b1,b2],
[x1,x2])
= max (
(dist (b1,x1)),
(dist (b2,x2)))
by Th18;
dist (
b2,
x2)
<= max (
(dist (b1,x1)),
(dist (b2,x2)))
by XXREAL_0:25;
then A67:
dist (
b2,
x2)
< r1
by A65, A66, A63, XXREAL_0:2;
reconsider x2i =
x2,
b2i =
b2 as
Element of
REAL j ;
reconsider b1i =
b1,
x1i =
x1 as
Element of
REAL i ;
consider b1f,
b2f being
FinSequence of
REAL such that A68:
(
b1f = b1 &
b2f = b2 )
and A69:
f . (
b1,
b2)
= b1f ^ b2f
by A3;
A70:
(
len b1f = i &
len b2f = j )
by A68, CARD_1:def 7;
dist (
b1,
x1)
<= max (
(dist (b1,x1)),
(dist (b2,x2)))
by XXREAL_0:25;
then
dist (
b1,
x1)
< r1
by A65, A66, A63, XXREAL_0:2;
then A71:
((Pitag_dist i) . (b1i,x1i)) + ((Pitag_dist j) . (b2i,x2i)) < r1 + r1
by A67, XREAL_1:8;
(
0 <= Sum (sqr (b1i - x1i)) &
0 <= Sum (sqr (b2i - x2i)) )
by RVSUM_1:86;
then
sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= |.(b1i - x1i).| + (sqrt (Sum (sqr (b2i - x2i))))
by SQUARE_1:59;
then
sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= ((Pitag_dist i) . (b1i,x1i)) + |.(b2i - x2i).|
by EUCLID:def 6;
then A72:
sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= ((Pitag_dist i) . (b1i,x1i)) + ((Pitag_dist j) . (b2i,x2i))
by EUCLID:def 6;
consider x1f,
x2f being
FinSequence of
REAL such that A73:
(
x1f = x1 &
x2f = x2 )
and A74:
f . (
x1,
x2)
= x1f ^ x2f
by A3;
A75:
(
len x1f = i &
len x2f = j )
by A73, CARD_1:def 7;
(Pitag_dist (i + j)) . (
fbb,
fxx) =
|.(fbb - fxx).|
by EUCLID:def 6
.=
sqrt (Sum (sqr (abs (fbb - fxx))))
by EUCLID:25
.=
sqrt (Sum (sqr ((abs (b1i - x1i)) ^ (abs (b2i - x2i)))))
by A65, A68, A69, A73, A74, A70, A75, Th15
.=
sqrt (Sum ((sqr (abs (b1i - x1i))) ^ (sqr (abs (b2i - x2i)))))
by Th10
.=
sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (abs (b2i - x2i)))))
by RVSUM_1:75
.=
sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (b2i - x2i))))
by EUCLID:25
.=
sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i))))
by EUCLID:25
;
then
dist (
fb,
fx)
< r
by A72, A71, XXREAL_0:2;
then
f . b in Ball (
fx,
r)
by METRIC_1:11;
hence
b in f " P
by A61, A64, FUNCT_2:38;
verum
end;
f " P is
Subset of
(max-Prod2 ((Euclid i),(Euclid j)))
by A5, TOPMETR:12;
then
f " P in Family_open_set (max-Prod2 ((Euclid i),(Euclid j)))
by A58, PCOMPS_1:def 4;
hence
f " P in the
topology of
[:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]
by A5, TOPMETR:12;
PRE_TOPC:def 2 verum
end;
[#] (TopSpaceMetr (Euclid (i + j))) <> {}
;
hence
f is continuous
by A56, TOPS_2:43; ( f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj ) )
[#] (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) <> {}
;
hence
f " is continuous
by A27, A5, TOPS_2:43; for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj
let fi, fj be FinSequence; ( [fi,fj] in dom f implies f . (fi,fj) = fi ^ fj )
assume A76:
[fi,fj] in dom f
; f . (fi,fj) = fi ^ fj
then reconsider Fi = fi as Element of the carrier of (Euclid i) by A1, A5, A4, ZFMISC_1:87;
reconsider Fj = fj as Element of the carrier of (Euclid j) by A76, A1, A5, A4, ZFMISC_1:87;
S1[Fi,Fj,f . (Fi,Fj)]
by A3;
hence
f . (fi,fj) = fi ^ fj
; verum